Supporting UML-based development of embedded systems by formal techniques |
| |
| Authors: | Jozef Hooman Hillel Kugler Iulian Ober Anjelika Votintseva Yuri Yushtein |
| |
| Affiliation: | (1) Embedded Systems Institute, Eindhoven, The Netherlands;(2) Radboud University, Nijmegen, The Netherlands;(3) New York University, New York, NY, USA;(4) Toulouse-II University, Toulouse, France;(5) CT SE 1 Siemens AG, Munich, Germany;(6) CIMSOLUTIONS B.V., Vianen, The Netherlands |
| |
| Abstract: | 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.
This work has been supported by EU-project IST 33522 – OMEGA “Correct Development of Real-Time Embedded Systems in UML”. For
more information, see . During this project, the second author was at theWeizmann Institute of Science, the third author at VERIMAG, the fourth
author at OFFIS, and the fifth author at NLR. |
| |
| Keywords: | Formal methods UML Embedded systems Real-time |
| 本文献已被 SpringerLink 等数据库收录！ |
|
