Publikation
Checking Concurrent Behavior in UML/OCL Models
Nils Przigoda; Christoph Hilken; Robert Wille; Jan Peleska; Rolf Drechsler
In: Timothy Lethbridge; Jordi Cabot; Alexander Egyed (Hrsg.). Proceedings of the 18th International Conference on Model Driven Engineering Languages and Systems. ACM/IEEE International Conference on Model Driven Engineering Languages and Systems (MoDELS-2015), September 27 - October 2, Ottawa, ON, Canada, Pages 176-185, ISBN 978-1-4673-6908-4, CEUR-WS.org, 2015.
Zusammenfassung
The Unified Modeling Language (UML) is a defacto standard for software development and, together with the Object Constraint Language (OCL), allows for a precise description of a system prior to its implementation. At the same time, these descriptions can be employed to check the consistency and, hence, the correctness of a given UML/OCL model. In the recent past, numerous (automated) approaches have been proposed for this purpose. The behavior of the systems has usually been considered by means of sequence diagrams, state machines, and activity diagrams. But with the increasing popularity of design by contract, also composite structures, classes, and operations are frequently used to describe behavior in UML/OCL. However, for these description means no solution for the validation and verification of concurrent behavior is available yet. In this work, we propose such a solution. To this end, we discuss the possible interpretations of “concurrency” which are admissible according to the common UML/OCL interpretation and, afterwards, propose a methodology which exploits solvers for SAT Modulo Theories (i. e., SMT solvers) in order to check the concurrent behavior of UML/OCL models. How to address the resulting problems is described and illustrated by means of a running example. Finally, the application of the proposed method is demonstrated.