Towards UML-based formal specifications of component-based real-time software
Towards UML-based formal specifications of component-based real-time software
复制标题
迈向基于组件的实时软件的基于 UML 的形式化规范
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
G. Occorso
中科院分区：
文献类型：
--
作者：
V. D. Bianco;L. Lavazza;M. Mauri;G. Occorso
UML-RT作为一种实时应用程序的建模语言，正变得越来越流行。不幸的是，UML-RT没有正式定义，它不适合支持规范阶段：例如，它不提供表示时间和非确定性的本机构造。UML+是UML的一个扩展，它是形式上定义良好的，适合于表达实时系统的规范（例如，UML+模型的属性可以被形式化验证）。但是，UML+不支持设计和开发。本文讨论了UML+到UML-RT的转换，从而为一个开发框架奠定了基础，在这个框架中，UML+和UML-RT一起使用，以消除彼此的限制。规范使用UML+编写，它们通过形式化方法自动验证，然后通过半自动过程转换为等效的UML-RT模型，该模型成为实现的起点。
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’s limitations. Specifications are written using UML+, they are automatically verified by means of formal methods, and are then converted – through a semi-automatic process – in an equivalent UML-RT model that becomes the starting point for the implementation.