UML-based Development of Embedded Systems by Formal Techniques
Jozef Hooman, Hillel Kugler, Iulian Ober, Anjelika Votintseva, and Yuri Yushtein
Software and Systems Modeling,
Volume 7, Number 2, pages 131-155, 2008.
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 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.