Technical report announcement



Date view Thread view Subject view Author view

Dino Distefano (ddino@cs.utwente.nl)
Fri, 07 Apr 2000 14:01:45 +0200


Dear pUML members, the following technical report may interest you. ============================ On a Temporal Logic for Object-Based Systems Dino Distefano, J.-P. Katoen, and Arend Rensink. Technical report CTIT 00-06, University of Twente, 2000. 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), an optional part of the UML standard for expressing static properties over class diagrams. 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. Keywords: formal verification, Object Constraint Language (OCL), object-based system, property specification, temporal logic. ============================= It is available at http://wwwhome.cs.utwente.nl/~ddino/report.html Regards, Dino Distefano


Date view Thread view Subject view Author view