|
doi: 10.3850/978-3-9815370-4-8_0646
Assisted Generation of Frame Conditions for Formal Models
Philipp Niemann1,a, Frank Hilken1,b, Martin Gogolla1,c and Robert Wille1,2,d
1Institute of Computer Science, University of Bremen, Bremen, Germany.
apniemann@informatik.uni-bremen.de
bfhilken@informatik.uni-bremen.de
cgogolla@informatik.uni-bremen.de
drwille@informatik.uni-bremen.de
2Cyber Physical Systems, DFKI GmbH, Bremen, Germany
ABSTRACT
Modeling languages such as UML or SysML allow for the validation and verification of the structure and the behavior of designs even in the absence of a specific implementation. However, formal models inherit a severe drawback: Most of them hardly provide a comprehensive and determinate description of transitions from one system state to another. This problem can be addressed by additionally specifying so-called frame conditions. However, only naive “workarounds“ based on trivial heuristics or completely relying on a manual creation have been proposed for their generation thus far. In this work, we aim for a solution which neither leaves the burden of generating frame conditions entirely on the designer (avoiding the introduction of another time-consuming and expensive design step) nor is completely automatic (which, due to ambiguities, is not possible anyway). For this purpose, a systematic design methodology for the assisted generation of frame conditions is proposed.
Full Text (PDF)
|