Towards Model Checking OCL

Share/Save/Bookmark

Distefano, Dino and Katoen, Joost-Pieter and Rensink, Arend (2000) Towards Model Checking OCL. In: ECOOP 2000: Defining Precise Semantics for UML, 12 June 2000, Sophia Antipolis, France.

[img]PDF
Restricted to UT campus only
: Request a copy
165Kb
Abstract:This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL). Eventually, the aim is to do model checking. The formal semantics of BOTL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL and, at the same time, permitting model checking of OCL constraints.
Item Type:Conference or Workshop Item
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/61727
Official URL:http://www.dcs.qmul.ac.uk/~ddino/papers/puml2k.pdf
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page