Deductive Verification of UML Models in TLPVS
Hillel Kugler, Amir Pnueli, and Mark van der Zwaag
Appeared in: Proceedings UML 2004,
LNCS 3273, Springer-Verlag, pp. 335-349, 2004.
In recent years, UML has been applied to the development
of reactive safety-critical systems, in which the quality of the developed
software is a key factor. In this paper we present an approach for the
deductive verification of such systems using the PVS interactive theorem
prover. Using a PVS specification of a UML kernel language semantics,
we generate a formal representation of the UML model. This representation
is then verified using tlpvs, our PVS-based implementation of
linear temporal logic and some of its proof rules. We apply our method
by verifying two examples, demonstrating the feasibility of our approach
on models with unbounded event queues, object creation, and variables
of unbounded domain. We define a notion of fairness for UML systems,
allowing us to verify both safety and liveness properties.