Modular formal verification of specifications of concurrent systems

摘要

In this paper, we propose a bottom-up approach for the verification of systems with modular structure: we prove that when the modules are composed in specific ways, the complete, software system verifies a composition of the properties each component does. We focus on the process of upgrading systems with new functionalities, where the validity of old requirements needs to be ensured, but also an understanding of the new properties the upgraded system would enjoy is useful. In this work, we assume each component to be specified by a CCS process, and the properties to be expressed by selective mu-calculus formulae.