Show simple item record

Automatic Analysis of Consistency Between Implementations and Requirements

dc.contributor.authorMarsha Chechik ,en_US
dc.contributor.authorGannon, Johnen_US
dc.description.abstractFormal 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)en_US
dc.format.extent513882 bytes
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3394en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-94-137en_US
dc.titleAutomatic Analysis of Consistency Between Implementations and Requirementsen_US
dc.typeTechnical Reporten_US
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtUMIACS Technical Reportsen_US

Files in this item


This item appears in the following Collection(s)

Show simple item record