Transformation of TOCL temporal properties into OCL
Transformation of TOCL temporal properties into OCL
复制标题
DOI：
10.1145/3550356.3563132
复制
发表时间：
2022-10
期刊：
影响因子：
--
通讯作者：
Mustafa Al-Lail;Antonio Rosales;Hector Cardenas;Lars Hamann;Alfredo J. Perez
中科院分区：
文献类型：
--
作者：
Mustafa Al-Lail;Antonio Rosales;Hector Cardenas;Lars Hamann;Alfredo J. Perez
指定和验证基于UML的系统的时态属性可能是具有挑战性的。尽管存在一些支持时态属性规范的OCL扩展，但大多数方法依赖于使用非UML形式，如LTL、CTL和CTL*。这些方法还依赖于将开发中的UML模型转换为非UML模型检查框架进行验证。这些方法引入了复杂性，并且依赖于不在UML范围内的技术和工具。在本文中，我们展示了如何将TOCL(用于时态属性规范的OCL扩展)转换为用于验证目的的OCL。为此，我们为TOCL创建了一个正式的EBNF语法，并在此基础上生成了一个解析器和一个MOF元模型。为了便于分析TOCL属性，我们使用QVTo形式化地定义了从TOCL元模型到OCL元模型的转换规则。我们使用USE验证了转换规则的实现。
Specifying and verifying the temporal properties of UML-based systems can be challenging. Although there exist some extensions of OCL to support the specification of temporal properties, most of the approaches depend on using non-UML formalisms such as LTL, CTL, and CTL*. The approaches also rely on transforming the under-development UML models into non-UML model checking frameworks for verification. These approaches introduce complexities and relies on techniques and tools that are not within the UML spectrum. In this paper, we show how TOCL (one OCL extension for temporal properties specification) can be transformed into OCL for verification purposes. Towards this end, we created a formal EBNF grammar for TOCL, based on which a parser and a MOF metamodel were generated. To facilitate the analysis of the TOCL properties, we formally defined transformation rules from the TOCL metamodel to the OCL metamodel using QVTo. We validated the implementations of the transformation rules using USE.