Formalizing UML Models and OCL Constraints in PVS

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 t...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2005-01, Vol.115, p.39-47
Main Authors: Kyas, Marcel, Fecher, Harald, de Boer, Frank S., Jacob, Joost, Hooman, Jozef, van der Zwaag, Mark, Arons, Tamarah, Kugler, Hillel
Format: Article
Language:English
Subjects:
Formal Semantics
Formal Verification
OCL
PVS
UML
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2004.09.027