Model checking of CTL-extended OCL specifications

被引：11

作者：

Bill, Robert ^{[1
]}

Gabmeyer, Sebastian ^{[1
]}

Kaufmann, Petra ^{[1
]}

Seidl, Martina ^{[2
]}

机构：

[1] Business Informatics Group, TU Wien, Austria

[2] Institute for Formal Models and Verification, JKU Linz, Austria

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8706卷

关键词：

Semantics - Temporal logic - Modeling languages - State space methods;

D O I：

10.1007/978-3-319-11245-9_13

中图分类号：

学科分类号：

摘要：

In software modeling, the Object Constraint Language (OCL) is an important language to specify properties that a model has to satisfy. The design of OCL reflects the structure of MOF-based modeling languages like UML and its tight integration results in an intuitive usability. But OCL allows to express properties only in the context of a single instance model and not with respect to a sequence of instance models that capture the execution of the system. In this paper, we show how OCL can be extended with CTL-based temporal operators to express properties over the lifetime of an instance model. We formally introduce syntax and semantics of our OCL extension cOCL. The properties specified with our OCL extension can be verified with our explicit state space model checking framework, called MocOCL. In a case study, we illustrate the expressiveness and usability of our approach and evaluate the performance of our implementation. © Springer International Publishing Switzerland 2014.

引用

页码：221 / 240