Detecting consistencies and inconsistencies of pattern-based functional requirements
Christian Ellen and Sven Sieverding and Hardi Hungar
Formal Methods for Industrial Critical Systems
The formal specifcation of functional requirements can often lead to inconsistency as well as unintended specifcation, especially in the early stages within the development process. In this paper, we present a formal model checking approach which tackles both of these problems and is also applicable during the requirements elicitation phase, in which no component model is available. The presented notion of consistency ensures the existence of at least one possible run of the system, which satisfes all requirements. To avoid trivial execution traces, the "intended" functional behavior of the requirements is triggered. The analysis is performed using model checking. More specifcally, to reduce the overall analysis efort, we apply a bounded model checking scheme. If the set of requirements is inconsistent the method also identifes a maximal sub-set of consistent requirements. Alternatively, a minimal inconsistent sub-set can be computed. The approach is demonstrated on a railway crossing example using the BTC Embedded Speci?er and the iSAT model checker.
2014
inproceedings
Springer Switzerland
Lecture Notes in Computer Science
155-169
CRYSTAL
Critical System Engineering Acceleration (sorry - only available in German)
Critical System Engineering Acceleration (sorry - only available in German)
Frédéric Lang and Francesco Flammini
8718
