A Formal Verification Environment for Distributed Object-Oriented Models

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.<br> 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.<br> 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.<br> 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