Formal Verification of UML-RT Capsules using Model Checking

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
117319.pdfFulltext1.98 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Formal Verification of UML-RT Capsules using Model Checking
Authors: Carlsson, Mats G I
Johansson, Lars G
Abstract: Formal 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.
Keywords: Programvaruteknik;Datorteknik;Software Engineering;Computer Engineering
Issue Date: 2009
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
Collection:Examensarbeten för masterexamen // Master Theses

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