Formalizing UML Models and OCL Constraints in PVS

被引：45

作者：

Kyas, Marcel ^{[1
]}

Fecher, Harald ^{[1
]}

de Boer, Frank S. ^{[2
]}

Jacob, Joost ^{[2
]}

Hooman, Jozef ^{[3
]}

van der Zwaag, Mark ^{[3
]}

Arons, Tamarah ^{[4
]}

Kugler, Hillel ^{[4
]}

机构：

[1] Christian Albrechts Univ Kiel, Inst Comp Sci & Appl Math, Kiel, Germany

[2] CWI, Amsterdam, Netherlands

[3] Univ Nijmegen, Comp Sci Dept, Nijmegen, Netherlands

[4] Weizmann Inst Sci, Rehovot, Israel

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2005年 / 115卷

关键词：

OCL; PVS; Formal Verification; Formal Semantics; UML;

D O I：

10.1016/j.entcs.2004.09.027

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：39 / 47

页数：9

共 13 条

[1]

Boldsoft and Rational Software Corporation and IONA and Adaptive Ltd, 2003, RESP UML 2 0 OCL REP

[2]

Brucker A. D., 2002, Theorem Proving in Higher Order Logics. 15th International Conference, TPHOLs 2002. Proceedings (Lecture Notes in Computer Science Vol.2410), P99

[3]

de Boer F. S., 2002, Formal Methods for Open Object-Based Distributed Systems V. IFIP TC6/WG6.1. Fifth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2002), P163

[4]

de Roever Willem-Paul, 2001, CONCURRENCY VERIFICA

[5]

Hooman Jozef, 2003, SVERTS

[6]

Nipkow Tobias, 2002, LNCS, V2283

[7]

Object Management Group, 2003, UML 2 0 INFR SPEC

[8]

Object Management Group, 2003, UML 2 0 SUP SPEC

[9]

OWRE S, 1992, LNAI, V607, P748

[10]

Pnueli Amir, 2003, LNCS, V2772

← 1 2 →