Supporting UML-based development of embedded systems by formal techniques

Jozef Hooman; Hillel Kugler; Iulian Ober; Anjelika Votintseva; Yuri Yushtein

Supporting UML-based development of embedded systems by formal techniques

Jozef Hooman ,
Hillel Kugler ,
Iulian Ober ,
Anjelika Votintseva ,
Yuri Yushtein

Software and Systems Modeling | May 2008 , Vol 7(2): pp. 131-155

Download BibTex

We describe an approach to support UMLbased development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts.We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions.