A Formal Verification Environment for Distributed Object-Oriented Models

dc.contributor.authorBaggiani, Giampiero
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T12:31:48Z
dc.date.available2019-07-03T12:31:48Z
dc.date.issued2011
dc.description.abstractDistributed 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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/136118
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectInformations- och kommunikationsteknik
dc.subjectProgramvaruteknik
dc.subjectInformation & Communication Technology
dc.subjectSoftware Engineering
dc.titleA Formal Verification Environment for Distributed Object-Oriented Models
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
Ladda ner
Original bundle
Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
136118.pdf
Storlek:
816.97 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext