Paper Info
Title
Formalizing UML Models and OCL Constraints in PVS
Abstract
The Object Constraint Language (OCL) is the established language for the specification of properties of objects and object structures in UML models. One reason that it is not yet widely adopted in industry is the lack of proper and integrated tool support for OCL. Therefore, we present a prototype tool, which analyzes the syntax and semantics of OCL constraints together with a UML model and translates them into the language of the theorem prover PVS. This defines a formal semantics for both UML and OCL, and enables the formal verification of systems modeled in UML. We handle the problematic fact that OCL is based on a three-valued logic, whereas PVS is only based on a two valued one.
Year
DOI
Venue
2005
10.1016/j.entcs.2004.09.027
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
pvs,ocl,uml model,prototype tool,object structure,problematic fact,formalizing uml models,established language,formal semantics,uml,integrated tool support,ocl constraint,ocl constraints,object constraint language,formal verification,system modeling,theorem prover
Programming language,Unified Modeling Language,UML tool,Computer science,Automated theorem proving,Applications of UML,Object Constraint Language,Syntax,Semantics,Formal verification
Journal
Volume
Issue
ISSN
115
C
1571-0661
Citations 
PageRank 
References 
46
2.76
7
Authors
8
Name
Order
Citations
PageRank
Marcel Kyas125827.57
H. Fecher227619.30
Frank S. de Boer32013159.02
Joost Jacob4462.76
Jozef Hooman552272.66
Mark Van Der Zwaag6765.00
Tamarah Arons727814.59
Hillel Kugler857735.87