Automated Validation & Verification of UML

Nils Przigoda · Robert Wille

Judith Przigoda · Rolf Drechsler

Automated Validation

& Veri cation of UML/

OCL Models Using

Satis ability Solvers

Automated Validation & Verification of UML/OCL

Models Using Satisfiability Solvers

Nils Przigoda • Robert Wille

Judith Przigoda • Rolf Drechsler

Automated Validation &

Verification of UML/OCL

Models Using Satisfiability

Solvers

123

Nils Przigoda

Mobility Division

Siemens AG

Braunschweig, Germany

Judith Przigoda

University of Bremen

Bremen, Germany

Robert Wille

Johannes Kepler University Linz

Linz, Austria

Rolf Drechsler

AG Rechnerarchitektur

University of Bremen

Bremen, Germany

Cyber-Physical Systems

DFKI GmbH, Bremen, Germany

ISBN 978-3-319-72813-1 ISBN 978-3-319-72814-8 (eBook)

https://doi.org/10.1007/978-3-319-72814-8

Library of Congress Control Number: 2017961733

© Springer International Publishing AG 2018

This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of

the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,

broadcasting, reproduction on microfilms or in any other physical way, and transmission or information

storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology

now known or hereafter developed.

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication

does not imply, even in the absence of a specific statement, that such names are exempt from the relevant

protective laws and regulations and therefore free for general use.

The publisher, the authors and the editors are safe to assume that the advice and information in this book

are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or

the editors give a warranty, express or implied, with respect to the material contained herein or for any

errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional

claims in published maps and institutional affiliations.

Printed on acid-free paper

This Springer imprint is published by Springer Nature

The registered company is Springer International Publishing AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

Preface

Only four decades after the first manned flight to the moon, a common device

such as a smartphone consists of more complex technology than the “high-end”

computers that controlled the Apollo 11 space mission. The same holds for software

which became more complex at an even higher rate. Consequently, the design of

such systems became a tremendously hard, difficult, and expensive problem. To

cope with this, modeling languages such as UML and SysML were introduced as

description means to describe quasi-blueprints in early stages of the design flow.

These modeling languages hide implementation details while providing a formal

base for the first system analysis.

However, in order to benefit from this abstraction, it has to be ensured that

the resulting models are applicable (motivating validation) and correct (motivating

verification). But even at this high level of abstraction, this remains a complex

problem. Accordingly, researchers heavily investigated the validation and verifi￾cation of UML/OCL models as well as models described in similar languages.

Solutions which are based on so-called satisfiability solvers find particular interests

due to their capability to completely cover large search spaces in a—considering the

usually exponential complexity—rather efficient fashion.

This book provides a comprehensive description of such methods and their

application—including a general flow that utilizes a formalization of UML/OCL.

While the presented flow focuses on using satisfiability solvers, how the provided

descriptions can additionally be used for any other automatic reasoning engine is

also described. Furthermore, for a broad variety of validation and verification tasks,

the application of the proposed flow is described. Additionally, the book also briefly

covers how nonfunctional properties such as timing constraints can be handled

within the described flow.

A case study demonstrates the possibilities and applicability of the presented

approaches and shows that there is still a gap between the UML/OCL models and

the following design steps. In order to address this problem, finally, an approach

is presented which verifies an implementation against its model. This enables

the designer to transfer validation and verification results to the following lower

abstraction levels.

v

vi Preface

This book is the result of several years of intensive research at the University of

Bremen, Germany; DFKI GmbH Bremen, Germany; the Johannes Kepler Univer￾sity Linz, Austria; and, recently, Siemens AG in Braunschweig, Germany. During

this time, we experienced broad support from many people for which we would like

to thank them very much. Most importantly, we are thankful to the respective groups

in Bremen, Linz, and Braunschweig for providing a comfortable and inspirational

environment from which some authors benefit until today. Particular thanks go to

(in alphabetical order) Christoph Hilken, Frank Hilken, Jannis Stoppe, Jan Peleska,

Jonas Gomes Filho, Julia Seiter, Martin Gogolla, Mathias Soeken, Pablo González

de Aledo, Pablo Sánchez Espeso, Philipp Niemann, and Ulrich Kühne for the

very productive collaboration that resulted in research papers which are partially

covered in this book. With respect to funding, we are indebted to thank the German

Research Foundation (DFG) which supported the research summarized in this book

through the Reinhart Koselleck project under grant no. DR 287/23-1, the Graduate

School SyDe funded by the German Excellence Initiative within the University of

Bremen’s institutional strategy, and the German Ministry of Education and Research

(BMBF) for their support through the projects SPECifIC under grant no. 01IW1300

and SELFIE under grant no. 01IW16001. Besides that, the Siemens AG Mobility

Division sponsored a scholarship for Nils Przigoda’s PhD thesis leading to several

results which formed the basis for this book. Finally, we would like to thank

Springer and, in particular, Charles “Chuck” Glaser, for making this book possible.

Braunschweig, Germany Nils Przigoda

Linz, Austria Robert Wille

Bremen, Germany Judith Przigoda

Bremen, Germany Rolf Drechsler

October 2017

Contents

1 Introduction .................................................................. 1

2 A Formal Interpretation of UML/OCL ................................... 7

2.1 Type System ............................................................. 8

2.2 Classes and Models ..................................................... 10

2.3 Objects and System States.............................................. 14

2.4 Invariants, Pre-, and Postconditions.................................... 16

2.5 Decision Problems ...................................................... 19

2.5.1 Boolean Satisfiability ........................................... 19

2.5.2 Satisfiability Modulo Theories ................................. 22

3 A Symbolic Formulation for Models....................................... 25

3.1 A General Flow for Automatic Verification and Validation........... 27

3.2 Transforming a Model into a Symbolic Formulation.................. 30

3.2.1 Transforming Attributes ........................................ 31

3.2.2 Transforming Associations..................................... 40

3.2.3 Handling a Fixed and Variable Number of Objects ........... 44

3.2.4 Handling Null and Invalid ...................................... 49

3.2.5 Transforming OCL Constraints ................................ 53

3.3 Adding Verification Tasks .............................................. 83

3.3.1 Structural Verification Tasks ................................... 83

3.3.2 Behavioral Verification Tasks .................................. 85

3.4 Other Approaches for Model Validation and Verification............. 92

4 Structural Aspects ........................................................... 95

4.1 Debugging Inconsistent Models........................................ 96

4.1.1 Problem Formulation ........................................... 97

4.1.2 Previously Proposed Solutions................................. 98

4.1.3 Proposed Approach ............................................. 100

4.1.4 Implementation and Evaluation ................................ 103

vii

viii Contents

4.1.5 Comparison with Other Approaches, Also from

Different Fields ................................................. 108

4.1.6 Example of Use ................................................. 109

4.2 Analyzing Invariant Independence ..................................... 110

4.2.1 Independence in Formal Models ............................... 111

4.2.2 Analysis for Invariant Independence........................... 113

4.2.3 Proposed Solution .............................................. 115

4.2.4 Experimental Evaluation ....................................... 118

4.3 Relation to Similar Approaches Used in SAT/SMT Solving ......... 121

5 Behavioral Aspects........................................................... 125

5.1 Restricting State Transitions Using Frame Conditions................ 126

5.1.1 Related Work.................................................... 127

5.1.2 Integrating Frame Conditions in the Symbolic Formulation.. 128

5.1.3 Deriving Frame Conditions from the AST .................... 138

5.2 Moving on to Concurrent Behavior in the Symbolic Formulation.... 144

5.2.1 Problem Formulation and Related Work ...................... 144

5.2.2 Handling Contradictory Conditions............................ 151

5.2.3 Implementation and Application ............................... 154

6 Timing Aspects ............................................................... 159

6.1 Preliminaries About Clocks and Ticks ................................. 161

6.2 A Generic Representation of CCSL Constraints ...................... 163

6.2.1 Determining the Generic Representation ...................... 164

6.2.2 Discussion and Application of the Generic Representation .. 168

6.3 Validation of Clock Constraints Against Instant Relations ........... 172

6.3.1 Motivation and Proposed Idea ................................. 173

6.3.2 Implementation ................................................. 175

6.3.3 Application and Evaluation .................................... 180

7 Reducing Instance Sizes with Ground Setting Properties ............... 183

7.1 Considered Running Example .......................................... 184

7.1.1 Considered Scenario ............................................ 184

7.1.2 Corresponding UML/OCL Model ............................. 185

7.2 Transformation of OCL Invariants and Resulting Problem ........... 187

7.2.1 Transformation of OCL Invariants............................. 187

7.2.2 Consequences and Resulting Problem ......................... 190

7.3 Ground Setting Properties for Efficient Transformation of OCL ..... 191

7.3.1 Ground Setting Properties...................................... 191

7.3.2 Efficient Transformation of OCL .............................. 193

7.4 Discussion and Related Work .......................................... 194

7.5 Implementation and Evaluation ........................................ 196

7.5.1 Implementation ................................................. 196

7.5.2 Evaluation ....................................................... 197

Contents ix

8 Re-utilizing Verification Results of UML/OCL Models.................. 201

8.1 What Can Be Verified Where?—A Case Study ....................... 202

8.1.1 Considered Access Control System............................ 202

8.1.2 Resulting Model ................................................ 203

8.1.3 Verification of the Model ....................................... 205

8.1.4 Implementation of the Model .................................. 210

8.1.5 Comparison to the Formal Model .............................. 213

8.1.6 Open Issues ..................................................... 217

8.2 Verifying Implementations Against Their Formal Specification...... 217

8.2.1 Envisioned Design Flow........................................ 218

8.2.2 General Idea..................................................... 220

8.2.3 Representation of the Implementation ......................... 222

8.2.4 Evaluation ....................................................... 227

9 Conclusion .................................................................... 235

Appendix A Class Inheritance ................................................ 239

Appendix B An SMT Instance with an Unknown Result .................. 241

Appendix C Contradictory XOR Definitions ................................ 243

References......................................................................... 245

Nomenclature

B B D ftrue; falseg

N N D f0; 1; 2; : : :g

Z Z D f:::; 1; 0; 1; 2; : : :g

– Symbol for null in OCL

? Symbol for invalid in OCL

˛

a Variable for the attribute a of the object in the symbolic representation

ˇc A variable indicating if objects of a class c exist or not

!!0 Variable for the operation to be executed during the transition from the

system state to 0

.

ı

a Definedness of an attribute a of the object in the symbolic representation

i=I A transformed OCL expression i or a set of OCL expressions I

 A set of links

 A single link, i.e., an instance of an association r



rolec2 Variable for possible links of rolec2 of the object in the symbolic

representation

E The set of all enumerations

V The set of all variables of all types

Vt The set of all variables with the type t

! An operation call ! D .; o/

˝m; The set of all operation calls

; 4 Inheritance relation between two classes

 The Greek letter  is used for a transformed value of a literal or the

result a transformed subexpression—in both cases combined a ı-variable

to ensure the pair notation .; ı/

A single system state of a model m

˙m The set of all possible system states of a model m

 The underbracket is used in SMT-LIB listing to show that term above must

be replaced by a precise value or number

A Attributes of a class

C The finite set of classes of a model m

xi

xii Nomenclature

c A single class c D .A; O;I/

F A finite set of frame conditions of an operation o

I Invariants of a class

m A (UML/OCL) model m D .C; R/

O Operations of a class

o A single operation of class o D .P;r; C; B/

P A maybe empty set of parameters of an operation o

R The finite set of associations between the classes of a model m

r A single association r D .rolec1 W c1;rolec2 W c2; .l1; u1/; .l2; u2//

r Return value of an operation o

v W t A variable with identifier v and type t 2 T

C A may empty set of preconditions of an operation o

C The (infinite) set of all classes

R The (infinite) set of all associations also called relations

T Type system

B A may empty set of postconditions of an operation o

An object instance of a class c

 A set of object instances

Chapter 1

Introduction

In the last decades, all kinds of systems human beings are surrounded by have

become more and more electrified, miniaturized, and digitalized. They also got

more powerful and, thus, much more complex tasks can be solved nowadays.

Hence, it is not surprising that already in 2012—just 43 years after the first manned

spaceflight Apollo 11 with its crew Neil Armstrong, Edwin Aldrin, and Michael

Collins landed on the moon—navigation systems for automobiles are more powerful

and versatile than the Apollo Guidance Computer (AGC) used for the Apollo 11

project. However, the AGC is seen as the first embedded computer as it was only

a part of the control unit supporting other systems. Today, embedded systems are

nearly everywhere. Examples for (embedded) systems are, on the one side, actively

used systems such as smartphones, smartwatches, or fitness bracelets and, on the

other side, hidden systems running in the background of other devices like anti￾blocking systems and airbags in cars.

With the increasing performance and complexity of systems, also their func￾tionality has increased and it keeps in doing so. Furthermore, there is currently no

indication that this will change in the next years, since all those systems are more

and more connected, thanks to 3G/4G/5G or, generally spoken, a globally connected

world. All this affects the design process of both, hardware and software, and

increases the problems designers have to consider. Consequently, the complexity of

both design processes increased, old methodologies need to be updated or discarded,

and completely new concepts have to be developed.

One of those new concepts is the strive for (higher) abstraction levels during

the system design. Generally, all first drafts of systems are specifications usually

provided in natural language. The contained information is coming from the

customers and/or users. They are often also the base for a contract between the

customer and the contractor, maybe also between a contractor, sub-contractor, and

suppliers. However, specifications are full of ambiguities caused by the richness of

words and languages, and/or communication problems. This makes it hard to answer

© Springer International Publishing AG 2018

N. Przigoda et al., Automated Validation & Verification of UML/OCL Models

Using Satisfiability Solvers, https://doi.org/10.1007/978-3-319-72814-8_1

1

2 1 Introduction

the questions are we building the right system (associated with the term validation)

and are we building the system right (associated with the term verification).

Therefore, hardware systems are not any longer designed in one step as a gate

list on a sheet of paper derived from a specification—this also holds for software

systems and assembly code in a similar fashion, i.e., normally no one will start to

write machine specific code after reading a specification. Instead, several abstraction

levels have been introduced for both hardware and software systems.

Nowadays, software programmers usually do not manually write assembly code

or take care of the interaction between software and hardware (on which the

software will run later); also punched tapes are out. In contrast to this, they use

object-oriented or functional programming languages and available compilers to

generate executable files. Those programming languages themselves are one or

more abstraction levels. For hardware systems, the current design flow already

includes several abstraction levels, e.g., the electronic system level and the register

transfer level.

However, the gap between the first prototypes and the specification is still

challenging. To close this gap and, at the same time, to overcome ambiguities

in the interpretation of the specification, a new abstraction level in between was

installed. In general, this abstraction level makes use of mathematical concepts to

describe system structure and behavior, represented by models that can—as their

syntax is usually quite close to natural language—easily be understood even by

non-mathematically-skilled people. In the domain of hardware design, this level

was recently introduced as the Formal Specification Level (FSL) [DSW12, Soe13].

For software, this concept of modeling languages is used for even longer. In both

cases, the concept of a (formal) modeling level combines the intuitive understanding

people have for a language close to natural language with the formal nature of

a mathematical description, making it evaluable by computers as well as human

beings. Hence, the chosen modeling language for this new level should be as easy

as possible to understand for all involved stakeholders, e.g., project managers,

developers, and clients. At the same time, the syntax has to be supported by a sound

mathematical background and semantics.

Representatives of recent modeling languages are the Unified Modeling Lan￾guage (UML, first versions go back to 1994), Alloy (1997), and the Systems

Modeling Language (SysML, 2003, an extension of UML 2.0 using its profiles).

Since these modeling languages allow the application of formal methods and are

an interesting new abstraction level, they received much attention in the recent past.

Most of the approaches presented in this book make use of UML—but many of them

can easily be adjusted, e.g., for SysML as well. Besides that, for non-functional

descriptions, we will additionally consider the Modeling and Analysis of Real-time

and Embedded systems (MARTE) framework.

However, for an adequate description of a system model, UML or a derivative

alone would not be sufficient in a general case. In fact, not before combined, e.g.,

with the Object Constraint Language (OCL), it is possible to define a UML model

of a system that respects a significant amount of details of a specification. For

this purpose, the declarative language OCL is used to annotate UML models with

1 Introduction 3

additional constraints. For example, so-called OCL invariants are typically used

to detail structural (or static) aspects of a model. Moreover, following the Design￾by-Contract concept [MNM87], the behavior of an operation can be described by

annotating so-called pre- and postconditions to a UML model. Motivated by this,

class diagrams as provided by UML can indeed be used as an all-purpose tool to

rather comprehensively model the structure and behavior of a system.

However, having a formal description alone is only a small improvement com￾pared to the ambiguities of a (natural language) specification. If the model already

contains design flaws at this stage, the formal description would be completely

useless in the worst case. Thus, it becomes crucial to validate and verify that

the system model is correct. As UML/OCL models are formally defined (or, at

least, a formal interpretation can be employed), they allow for the application of

different formal methods for validation and verification (V&V) purposes. Due to

their capability of formally defining a system, UML/OCL models are also called

formal models in the following.

Assuming now that formal methods are available to validate and verify the formal

models, it is possible to prove that certain properties are satisfied or violated before

any implementation steps are done. Hence, models can be seen as a blueprint

of the system to be built in which errors can be detected early in the design

process. Moreover, in most cases, even an automatic detection becomes possible.

Consequently, the entire process of designing a new error-free system as well as the

burden of detecting and finding errors becomes less cumbersome and less expensive.

In this book, we will particularly cover the following checks:

• Does any valid instance of the model exist? Or in other words, is the model

consistent?

• Does a given model contain contradictory constraints? If yes, which constraints

are causing the contradiction?

• Does the model contain unwanted (in)dependencies? If yes, which constraints

are causing the unwanted dependencies?

• Can the system be executed at all? If yes, can the system get stuck in dead- or

livelocks?

• How can concurrent behavior of the system be analyzed using the formal model

and can this concurrent behavior of the system lead to problems?

• How can non-functional behavior, in particular timing-constraints, be consid￾ered?

• How can verification results be transferred to a lower abstraction level?

In the following chapters, all these questions are considered by analyzing and

improving existing solutions as well as proposing new methods to deal with the

different aspects of formal models.

For this purpose, a verification flow for formal models is proposed and described

in detail (cf. Fig. 3.1 on p. 28). The main idea of this flow is based on model

transformations and applying efficient solving engines in the target language. More

precisely, formal methods will not be applied directly at a formal model. Instead,

V&V tasks for a formal model are transformed into a decision problem. The great

4 1 Introduction

progress in the development of algorithms to tackle various decision problems made

this transformation very prominent [BieC09]. In fact, in the hardware domain, many

problems are transformed into an instance of the Satisfiability Problem (SAT), e.g.,

for test pattern generation [EWD13] and equivalence checking [GPB01, DS07].

Using so-called SAT solvers, solutions in huge search spaces can be determined in

an efficient fashion. In this book, we will use an extension of these SAT solvers,

i.e., solvers for Satisfiability Modulo Theories (SMT). SMT solvers are used as

a powerful and efficient black box in order to determine witnesses as well as

counterexamples for the given task. Overall, this forms a formal foundation on

which the remainder of this book is based on: The application of formal methods to

various aspects of model evaluation with respect to system design.

The combination of the model transformation and an SMT solver makes it

possible to apply those formal methods. As already mentioned above, this allows

for validation and verification of systems before any implementation steps are done.

Flaws in these system blueprints can also be analyzed and fixed earlier in the design

process—and in most cases also easier. In this book, we describe and illustrate how

this can be accomplished. To this end, the book is structured with respect to six main

pillars (each covered in a separate chapter):

• First, we provide a formalization of UML/OCL models as well as corresponding

background information, e.g., on UML/OCL in general and on decision problems

in Chap. 2. The formalization of UML/OCL models is an important first step that

allows to reason about a description afterwards. In fact, this formalization is used

in the following Chap. 3 to derive a symbolic formulation of all possible states

a UML/OCL model can assume. Based on this, validation and verification tasks

can be employed on top of it.

• A second pillar addresses questions about how to deal with structural aspects of

UML/OCL models, i.e., inconsistency and (in)dependencies. To this end, Chap. 4

introduces methods to automatically detect contradictions in UML/OCL models

as well as to aid the designer in identifying their source. Besides that, methods

are shown which help to identify (in)dependencies between the constraints. For

all these cases, the symbolic formulation will be utilized.

• Since the formal models are not restricted to structural aspects only, the third

pillar covered in Chap. 5 considers various behavioral aspects. This requires the

consideration of so-called frame conditions but, then, allows to check, e.g., for

issues such as reachability, live- and deadlocks, executability, etc. Besides that,

this chapter also discusses what has to be done when concurrent behavior is

assumed for a formal model.

• The fourth pillar leaves the sole functional consideration and additionally

considers timing as a non-functional property which may occur in corresponding

system descriptions. To this end, the symbolic formulation introduced before

is extended to descriptions provided in UML/MARTE models. By this, the

corresponding Chap. 6 shows the generality of the proposed solutions and, at

the same time, covers an important aspect of modern system designs.