SUML/PVS Tools

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.

SUML

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.

OCL

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

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 UML MARS example
• The UML prime-sieve example
• The Mips hardware example

OAS

Last modified by Joost Jacob, February 3, 2005.