Supporting UML-based development of embedded systems by formal techniques

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-timedmodel 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.

omega08.pdf
PDF file

In  Software and Systems Modeling

Publisher  Springer Verlag

Details

TypeArticle
URLhttp://dx.doi.org/10.1007/s10270-006-0043-7
Pages131-155
Volume7
Number2
> Publications > Supporting UML-based development of embedded systems by formal techniques