IST-2001-33522 OMEGA

Correct Development of Real-Time Embedded Systems

The OMEGA toolset

The OMEGA toolset
     Timed system verification
     Untimed system verification
     PVS tools
     LSC tools
The OMEGA UML profile
Case studies
Publications and bibliography
Download documents
Partners & Persons
Related links



We have implemented a tool that translates a subset of UML, as exported by certain case tools into the XMI format, to the input language of the theorem prover PVS. Because XMI allows for many variantions of the exported format, it is tedious to implement a reader for this format. To simplify this process, we have implemented a translation of two XMI dialects, namely the one of Rhapsody and the one of ArgoUML, to an intermediate format, which we call SUML.

We have implemented a translator from SUML to PVS. The same tool also reads and typechecks OCL constraints and generates corresponding proof obligations in PVS.

As an alternative, constraints can be specified directly in PVS. This also enables the use of TLPVS, which is a framework for proving linear-time temporal logic properties of UML models.


The SUML (simple UML) format is a simplified XML representation of UML models, which are commonly interchanged in the XMI format.

The issue with XMI is, that while it is a standard format for model exchange, it contains too much information, and is not really portable between different tools. Each tool may define its own variant of this format. To simplify the implementation of our tools, we defined a translation of subsets of the XMI format as implemented by Rhapsody and by Rational Rose into the SUML format.

Tools for translating XMI to SUML and PVS are available here.


The OCL Tool implements a translation of a subset of OCL constraints into the input language of the theorem prover PVS.

In order to avoid implementing a three-valued logic within the framework of PVS, we decided to define a sound translation of OCL into a two-valued logic. The advantage is a more direct representation of constraints in PVS. The disadvantage is, that a set of constraints, which are undefined in OCL, may be provable in PVS.

OCL is a three-valued logic, because the semantics was defined for an executable language and not a logic. If the evaluation of an expression raises an exception or diverges, then the constraint is considered to be undefined. However, such notions do not exist in the declarative semantics of a logic. Finally, for our purposes the provability of a constraint is more important than whether its execution may terminate.

The OCL tool is available here.


TLPVS is a PVS implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive LTL system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems - systems in which the number of processes is unbounded - and our - verification rules are appropriate to such systems.

TLPVS is available here.

We also provide some examples. They all run with April version of TLPVS:


The OMEGA Abstract Semantics (OAS) tool was called the RML-tool earlier, since the Rule Markup Language (RML) is used for its implementation. The OAS tool was designed for experimental analysis of the abstract OMEGA kernel model semantics.
The user provides a class diagram plus object diagram with the model to analyse. The user provides scripts in a scripting language that define the transformation semantics and the scheduling semantics.
An online version of the tool without scripting is available here.
The open-source software with scripting functionality is here.

Last modified by Joost Jacob, February 3, 2005.

You are currently authenticated as omegapublic (level 0)
For comments about this site please contact the webmaster