From Domain-Specific Language to Timed Automata. Automatic Translation and Verification of Contract Specifications

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/243893
Download file(s):
File Description SizeFormat 
243893.pdfFulltext488.65 kBAdobe PDFView/Open
Full metadata record
DC FieldValueLanguage
dc.contributor.authorGulliksson, Runa
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-03T14:21:27Z-
dc.date.available2019-07-03T14:21:27Z-
dc.date.issued2016
dc.identifier.urihttps://hdl.handle.net/20.500.12380/243893-
dc.description.abstractAnalysis of contracts is becoming an increasingly important subject due to the amount of agreements on the web. In this thesis a compositional formal language, Simplified Contract Language, SCL, is used to represent contracts. A translation between SCL and Timed Automata is designed and implemented, in order to verify contracts using temporal logic. UPPAAL is used as the timed automata verifying tool. The translation is shown to preserve the behavioral semantics of the SCL. The translation is tested thoroughly, using QuickCheck, against an implementation of the semantics in terms of trace acceptance. A case study of a university course, modeled as a contract, is done. It shows that it is possible to use the SCL and the translation for analyzing a real world contract with different traces. The case study also shows that when randomly generating events the state space can get large enough to slow down the verification speed significantly.
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectInformations- och kommunikationsteknik
dc.subjectData- och informationsvetenskap
dc.subjectInformation & Communication Technology
dc.subjectComputer and Information Science
dc.titleFrom Domain-Specific Language to Timed Automata. Automatic Translation and Verification of Contract Specifications
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
Collection:Examensarbeten för masterexamen // Master Theses



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