Towards Model Checking OCL


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
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
Additional information:Position paper
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page