Transformation of TOCL temporal properties into OCL

Abstract

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.