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 structures demands for a high reliability and thus, for in-depth functional verification. This thesis contributes to the development of a formal environment for the verification of Creol models. Creol is an executable modelling language featuring many aspects which make it very suitable for its employment in distributed, concurrent applications. The major contributions of this work are: the design of a formal specification language for Creol (CSL), the implementation of a front-end supporting inline specifications and its integration in the theorem prover KeY. CSL focuses on providing the user with an abstract way of expressing properties on communication traces between objects. It relies on a compositional proof system which allows the independent verification of object's methods against invariants and operation contracts.