Formal Verification of UML-RT Capsules using Model Checking

University essay from Chalmers tekniska högskola/Institutionen för data- och informationsteknik

Abstract: Formal verification methods have successfully been used to ensure correctnessof both hardware and software systems. In contrast to testing methods, thatcan demonstrate the presence of faults in a system, formal methods can provetheir absence.A department of the telecommunications company Ericsson AB in Gothenburg,Sweden, uses the UML-RT language to model software used in WCDMAradio base stations. These concurrent and reactive systems can be modeled inthe Eclipse-based RSARTE environment.Previous work underlines a need of narrowing the gap between softwaredevelopment tools used in industry and formal verification tools. This thesisexamines the feasibility of using model checking to verify properties of UMLRTcapsules. We present a prototype tool for generating verification modelsin the Promela language for the model checker Spin. The tool is implementedas a model-to-text transformation using the JET tool and is integrated intoRSARTE.The result of the work establishes that it, for a subset of constructs inUML-RT, is possible to automate generation of verification models that can beused to demonstrate properties of the original UML-RT capsules. We demonstratethis with example models created in RSARTE.