A Formal Verification Environment for Distributed Object-Oriented Models
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Publicerad
2011
Författare
Baggiani, Giampiero
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Informations- och kommunikationsteknik , Programvaruteknik , Information & Communication Technology , Software Engineering