Formal Verification of UML-RT Capsules using Model Checking

Visa enkel post
dc.contributor.authorCarlsson, Mats G I
dc.contributor.authorJohansson, Lars G
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:17:42Z
dc.date.available2019-07-03T12:17:42Z
dc.date.issued2009
dc.description.abstractFormal verification methods have successfully been used to ensure correctness of both hardware and software systems. In contrast to testing methods, that can demonstrate the presence of faults in a system, formal methods can prove their absence. A department of the telecommunications company Ericsson AB in Gothenburg, Sweden, uses the UML-RT language to model software used in WCDMA radio base stations. These concurrent and reactive systems can be modeled in the Eclipse-based RSARTE environment. Previous work underlines a need of narrowing the gap between software development tools used in industry and formal verification tools. This thesis examines the feasibility of using model checking to verify properties of UMLRT capsules. We present a prototype tool for generating verification models in the Promela language for the model checker Spin. The tool is implemented as a model-to-text transformation using the JET tool and is integrated into RSARTE. The result of the work establishes that it, for a subset of constructs in UML-RT, is possible to automate generation of verification models that can be used to demonstrate properties of the original UML-RT capsules. We demonstrate this with example models created in RSARTE.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/117319
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectProgramvaruteknik
dc.subjectDatorteknik
dc.subjectSoftware Engineering
dc.subjectComputer Engineering
dc.titleFormal Verification of UML-RT Capsules using Model Checking
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
117319.pdf
Storlek:
1.94 MB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen