TY - GEN
T1 - Frame conditions in symbolic representations of UML/OCL models
AU - Przigoda, Nils
AU - Filho, Jonas Gomes
AU - Niemann, Philipp
AU - Wille, Robert
AU - Drechsler, Rolf
N1 - Publisher Copyright:
© 2016 IEEE.
PY - 2016/12/27
Y1 - 2016/12/27
N2 - Verification and validation of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades - except for UML/OCL where corresponding approaches have been investigated only recently. Besides that, several approaches for the verification of the behavior specified in UML/OCL models have been proposed. They rely on a symbolic representation of all possible system states and transitions between them. But here, frame conditions have not been considered yet - a significant drawback for the underlying verification approaches. In this paper, we describe how to integrate frame conditions to symbolic representations. This enables designers to verify the behavior of UML/OCL models while, at the same time, respecting the given frame conditions.
AB - Verification and validation of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades - except for UML/OCL where corresponding approaches have been investigated only recently. Besides that, several approaches for the verification of the behavior specified in UML/OCL models have been proposed. They rely on a symbolic representation of all possible system states and transitions between them. But here, frame conditions have not been considered yet - a significant drawback for the underlying verification approaches. In this paper, we describe how to integrate frame conditions to symbolic representations. This enables designers to verify the behavior of UML/OCL models while, at the same time, respecting the given frame conditions.
UR - http://www.scopus.com/inward/record.url?scp=85010735040&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2016.7797747
DO - 10.1109/MEMCOD.2016.7797747
M3 - Conference contribution
AN - SCOPUS:85010735040
T3 - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
SP - 65
EP - 70
BT - 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 14th ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016
Y2 - 18 November 2016 through 20 November 2016
ER -