Nils Przigoda, Mathias Soeken, Robert Wille, Rolf Drechsler,
"Verifying the Structure and Behavior in UML/OCL Models Using Satisfiability Solvers"
, in IET Cyber-Physical Systems, Vol. 1, Nummer 1, Seite(n) 49-59, 2016, ISSN: 2398-3396
Original Titel:
Verifying the Structure and Behavior in UML/OCL Models Using Satisfiability Solvers
Sprache des Titels:
Englisch
Original Kurzfassung:
Due to the ever increasing complexity of embedded and cyber-physical systems, corresponding design solutions relying on modeling languages such as UML/OCL find increasing
attention. Because of 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, we motivate, define, and describe different verification tasks for structural as well
as behavioral UML/OCL models that can be solved using solvers for Boolean satisfiability. We
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.
Forschungs-