Verifying OCL specifications of UML models : tool support and compositionality

Leiden Repository

Verifying OCL specifications of UML models : tool support and compositionality

Type: Doctoral Thesis
Title: Verifying OCL specifications of UML models : tool support and compositionality
Author: Kyas, Marcel
Publisher: Lehmanns Media
Faculty of Mathematics and Natural Sciences, Leiden University
Issue Date: 2006-04-04
Keywords: D.2.4 [Software Engineering]: Software/Program Verification - formal methods;
F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - specification techniques
Abstract: The Unified Modelling Language (UML) and the Object Constraint Language (OCL) serve as specification languages for embedded and real-time systems used in a safety-critical environment. In this dissertation class diagrams, object diagrams, and OCL constraints are formalised. The formalisation serves as foundation for a translation of class diagrams, state machines, and constraints into the theorem prover PVS. This enables the formal verification of models defined in a subset of UML using the interactive theorem prover. The type system of OCL makes writing specifications difficult while the model is still under development. To overcome this difficulty a new type system is proposed, based on intersection types, union types, and bounded operator abstraction. To reduce the complexity of the model and to increase the structure of the specification, compositional reasoning is used. The introduction of history variables allows compositional specifications. Proof rules support compositional reasoning. The feasibility of the presented approach is demonstrated by two case-studies. The first one is the "Sieve of Eratosthenes" and the second one is a part of the medium altitude reconnaissance system (MARS) deployed in F-16 fighters of the Royal Dutch Air Force.
Description: Promotors: J.N. Kok, W.-P. de Roever, Co-Promotor: F.S. de Boer
With summary in Dutch
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Kyas, M., 2006, Doctoral thesis, Leiden University
Series/Report no.: IPA Dissertation Series ; 2006-05
ISBN: 3865411428
Sponsor: Part of this work has been financially supported by IST project OMEGA (IST-33522-2001) and NWO/DFG project Mobi-j (RO 1122/9-1, RO 1122/9-2). The work has been carried out at the Christian-Albrechts-Universität zu Kiel, Germany.

Files in this item

Description Size View
text/html Links to published articles 9.728Kb View/Open
application/pdf Cover 8.155Mb View/Open
application/pdf Title page_Pref ... of tables_List of figures 120.9Kb View/Open
application/pdf Chapter 1 162.5Kb View/Open
application/pdf Chapter 2 421.1Kb View/Open
application/pdf Chapter 3 278.6Kb View/Open
application/pdf Chapter 4 320.2Kb View/Open
application/pdf Chapter 5 248.5Kb View/Open
application/pdf Chapter 6 213.6Kb View/Open
application/pdf Chapter 7 226.1Kb View/Open
application/pdf Chapter 8 63.79Kb View/Open
application/pdf Appendices 110.2Kb View/Open
application/pdf Bibliography_Summary_Summary in Dutch_CV_ 215.6Kb View/Open
application/pdf Propositions 39.91Kb View/Open

This item appears in the following Collection(s)