A Formal Verification Environment for Distributed Object-Oriented Models

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/136118
Download file(s):
File Description SizeFormat 
136118.pdfFulltext816.97 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: A Formal Verification Environment for Distributed Object-Oriented Models
Authors: Baggiani, Giampiero
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.
Keywords: Informations- och kommunikationsteknik;Programvaruteknik;Information & Communication Technology;Software Engineering
Issue Date: 2011
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/136118
Collection:Examensarbeten för masterexamen // Master Theses

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.