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 lineartime 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 threevalued logic within the
framework of PVS, we decided to define a sound translation of
OCL into a twovalued 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 threevalued 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:
OAS
The OMEGA Abstract Semantics (OAS) tool was called the RMLtool
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 opensource software with scripting functionality is
here.
Last modified by Joost Jacob, February 3, 2005.
