A Formal Verification Environment for Distributed Object-Oriented Models

Abstract: Distributed systems are gaining increasing interest in the research community.The growing adoption of such systems for safety-critical structuresdemands for a high reliability and thus, for in-depth functional verification.
This thesis contributes to the development of a formal environment forthe verification of Creol models. Creol is an executable modelling languagefeaturing many aspects which make it very suitable for its employment indistributed, concurrent applications.
The major contributions of this work are: the design of a formal specificationlanguage for Creol (CSL), the implementation of a front-end supportinginline specifications and its integration in the theorem prover KeY.
CSL focuses on providing the user with an abstract way of expressingproperties on communication traces between objects. It relies on a compositionalproof system which allows the independent verification of object'smethods against invariants and operation contracts.