Towards UML-based formal specifications of component-based real-time software
International Journal on Software Tools for Technology Transfer (STTT), 9 (2):
179--192 (March 2007)DOI: 10.1007/s10009-006-0024-8
Abstract
UML-RT is achieving increasing popularity as a modeling language for real-time applications. Unfortunately UML-RT is not formally well defined and it is not well suited for supporting the specification stage: e.g., it does not provide native constructs to represent time and non-determinism. UML+ is an extension of UML that is formally well defined and suitable for expressing the specifications of real-time systems (e.g., the properties of a UML+ model can be formally verified). However, UML+ does not support design and development. This article addresses the translation of UML+ into UML-RT, thus posing the basis for a development framework where UML+ and UML-RT are used together, in order to remove each other^a€™s limitations. Specifications are written using UML+, they are automatically verified by means of formal methods, and are then converted ^a€“ through a semi-automatic process ^a€“ in an equivalent UML-RT model that becomes the starting point for the implementation.
