Formal Verification of UML-RT Capsules using Model Checking
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Publicerad
2009
Författare
Carlsson, Mats G I
Johansson, Lars G
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Programvaruteknik , Datorteknik , Software Engineering , Computer Engineering