TY - GEN
T1 - Checking concurrent behavior in UML/OCL models
AU - Przigoda, Nils
AU - Hilken, Christoph
AU - Wille, Robert
AU - Peleska, Jan
AU - Drechsler, Rolf
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/11/25
Y1 - 2015/11/25
N2 - 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.
AB - 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.
KW - Complex systems
KW - Computational modeling
KW - Concurrent computing
KW - Contracts
KW - Software
KW - Standards
KW - Unified modeling language
UR - http://www.scopus.com/inward/record.url?scp=84961613358&partnerID=8YFLogxK
U2 - 10.1109/MODELS.2015.7338248
DO - 10.1109/MODELS.2015.7338248
M3 - Conference contribution
AN - SCOPUS:84961613358
T3 - 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, MODELS 2015 - Proceedings
SP - 176
EP - 185
BT - 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, MODELS 2015 - Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2015
Y2 - 30 September 2015 through 2 October 2015
ER -