Frame Conditions in Symbolic Representations of UML/OCL Models
Sprache des Titels:
Englisch
Original Buchtitel:
International Conference on Formal Methods and Models for Codesign (MEMOCODE)
Original Kurzfassung:
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.
Forschungs-