Paper Info
Title
Deductive Verification of UML Models in TLPVS
Abstract
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.
Year
DOI
Venue
2004
10.1007/978-3-540-30187-5_24
Lecture Notes in Computer Science
Keywords
Field
DocType
formal verification,deductive verification,PVS,UML,state machines,semantics,temporal logic
Programming language,Unified Modeling Language,UML tool,Computer science,Theoretical computer science,Linear temporal logic,Applications of UML,Temporal logic,Proof assistant,Formal verification,Liveness
Conference
Volume
ISSN
Citations 
3273
0302-9743
13
PageRank 
References 
Authors
0.79
17
5
Name
Order
Citations
PageRank
Tamarah Arons127814.59
Jozef Hooman252272.66
Hillel Kugler357735.87
Amir Pnueli4129642377.59
Mark Van Der Zwaag5765.00