Assisted generation of frame conditions for formal models

Philipp Niemann, Frank Hilken, Martin Gogolla, Robert Wille

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

13 Scopus citations

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.

Original languageEnglish
Title of host publicationProceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages309-312
Number of pages4
ISBN (Electronic)9783981537048
DOIs
StatePublished - 22 Apr 2015
Externally publishedYes
Event2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015 - Grenoble, France
Duration: 9 Mar 201513 Mar 2015

Publication series

NameProceedings -Design, Automation and Test in Europe, DATE
Volume2015-April
ISSN (Print)1530-1591

Conference

Conference2015 Design, Automation and Test in Europe Conference and Exhibition, DATE 2015
Country/TerritoryFrance
CityGrenoble
Period9/03/1513/03/15

Fingerprint

Dive into the research topics of 'Assisted generation of frame conditions for formal models'. Together they form a unique fingerprint.

Cite this