Identifying domain axioms using binary decision diagrams

Barbara J. Czerny, Mats P.E. Heimdahl

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Statically analyzing requirements specifications to assure that they possess desirable properties is a useful activity in any rigorous software development project. The analysis is performed on an abstraction of the original requirements specification. The abstractions in the model may lead to spurious errors in the analysis output. Spurious errors are errors that are reported to occur under certain conditions, but information abstracted from the model precludes the conditions from being satisfied in the original model. A high ratio of spurious errors to true errors in the analysis output makes it difficult, error-prone, and time consuming to find and correct the true errors. In this paper we describe a technique that uses binary decision diagrams to help the analyst identify the abstractions that are lending to excessive spurious errors in the analysis output. Information about these abstractions can then be incorporated into the analysis to eliminate the corresponding spurious error reports.

Original languageEnglish (US)
Title of host publicationProceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages132-140
Number of pages9
ISBN (Electronic)0769504183, 9780769504186
DOIs
StatePublished - Jan 1 1999
Event4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999 - Washington, United States
Duration: Nov 17 1999Nov 19 1999

Publication series

NameProceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999

Other

Other4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
CountryUnited States
CityWashington
Period11/17/9911/19/99

Fingerprint Dive into the research topics of 'Identifying domain axioms using binary decision diagrams'. Together they form a unique fingerprint.

Cite this