Automatic Analysis of Consistency Between Implementations and Requirements
Automatic Analysis of Consistency Between Implementations and Requirements
Files
Publication or External Link
Date
1998-10-15
Authors
Marsha Chechik ,
Gannon, John
Advisor
Citation
DRUM DOI
Abstract
Formal methods like model checking can be used to demonstrate
that safety properties of embedded systems are enforced by the
system's requirements. Unfortunately, proving these properties
provides no guarantee that they will be preserved in an
implementation of the system. We have developed a tool, called
Analyzer, which helps discover instances of inconsistency and
incompleteness in implementations with respect to requirements.
Analyzer uses requirements information to automatically generate
properties which ensure that required state transitions appear in
a model of an implementation. A model is created through abstract
interpretation of an implementation annotated with assertions about
values of state variables which appear in requirements. Analyzer
determines if the model satisfies both automatically-generated and
user-specified safety properties.
This paper presents a description of our implementation of Analyzer
and our experience in applying it to a small but realistic problem.
(Also cross-referenced as UMIACS-TR-94-137)