Open AccessVerifying the structure and behavior in UML/OCL models using satisfiability solvers
Author(s) -
Przigoda Nils,
Soeken Mathias,
Wille Robert,
Drechsler Rolf
Publication year - 2016
Publication title -
iet cyber‐physical systems: theory and applications
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.308
H-Index - 7
ISSN - 2398-3396
DOI - 10.1049/iet-cps.2016.0022
Subject(s) - object constraint language , computer science , correctness , unified modeling language , applications of uml , programming language , uml tool , satisfiability , modeling language , formal verification , theoretical computer science , software
Due to the ever increasing complexity of embedded and cyber‐physical systems, corresponding design solutions relying on modelling languages such as Unified Modelling Language (UML)/Object Constraint Language (OCL) find increasing attention. Due to the recent success of formal verification techniques, UML/OCL models also allow to verify and/or check certain properties of a given model in early stages of the design phase. To this end, different approaches for verification and validation have been proposed. In this work, the authors motivate, define, and describe different verification tasks for structural, as well as behavioural UML/OCL models that can be solved using solvers for Boolean satisfiability. They describe how these verification tasks can be translated into a symbolic formulation which is passed to off‐the‐shelf solvers afterwards. The obtained results enable designers to draw conclusions about the correctness of the considered model.