Supporting UML-based Development of Embedded Systems by Formal Techniques

J. Hooman, H. Kugler, I. Ober, A. Votintseva and Y. Yushtein

We describe an approach to support UML-based 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 capture 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.

International Journal of Software and Systems Modeling