TY - GEN
T1 - Identifying domain axioms using binary decision diagrams
AU - Czerny, Barbara J.
AU - Heimdahl, Mats P.E.
PY - 1999/1/1
Y1 - 1999/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85040798174&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85040798174&partnerID=8YFLogxK
U2 - 10.1109/HASE.1999.809488
DO - 10.1109/HASE.1999.809488
M3 - Conference contribution
AN - SCOPUS:85040798174
T3 - Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
SP - 132
EP - 140
BT - Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
Y2 - 17 November 1999 through 19 November 1999
ER -