Identifying domain axioms using binary decision diagrams

Barbara J. Czerny; Mats P.E. Heimdahl

doi:10.1109/HASE.1999.809488

Identifying domain axioms using binary decision diagrams

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	132-140
Number of pages	9
ISBN (Electronic)	0769504183, 9780769504186
DOIs	https://doi.org/10.1109/HASE.1999.809488
State	Published - Jan 1 1999
Externally published	Yes
Event	4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999 - Washington, United States Duration: Nov 17 1999 → Nov 19 1999

Publication series

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

Other

Other	4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999
Country/Territory	United States
City	Washington
Period	11/17/99 → 11/19/99

Publisher link

10.1109/HASE.1999.809488

Find It

Find It at U of M Libraries

Cite this

Czerny, B. J., & Heimdahl, M. P. E. (1999). Identifying domain axioms using binary decision diagrams. In Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999 (pp. 132-140). Article 809488 (Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/HASE.1999.809488

Identifying domain axioms using binary decision diagrams. / Czerny, Barbara J.; Heimdahl, Mats P.E.
Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999. Institute of Electrical and Electronics Engineers Inc., 1999. p. 132-140 809488 (Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Czerny, BJ & Heimdahl, MPE 1999, Identifying domain axioms using binary decision diagrams. in Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999., 809488, Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999, Institute of Electrical and Electronics Engineers Inc., pp. 132-140, 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999, Washington, United States, 11/17/99. https://doi.org/10.1109/HASE.1999.809488

Czerny BJ, Heimdahl MPE. Identifying domain axioms using binary decision diagrams. In Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999. Institute of Electrical and Electronics Engineers Inc. 1999. p. 132-140. 809488. (Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999). doi: 10.1109/HASE.1999.809488

Czerny, Barbara J. ; Heimdahl, Mats P.E. / Identifying domain axioms using binary decision diagrams. Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999. Institute of Electrical and Electronics Engineers Inc., 1999. pp. 132-140 (Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999).

@inproceedings{14d3a4c37c894615bd11d7d07042a329,

title = "Identifying domain axioms using binary decision diagrams",

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.",

author = "Czerny, {Barbara J.} and Heimdahl, {Mats P.E.}",

year = "1999",

month = jan,

day = "1",

doi = "10.1109/HASE.1999.809488",

language = "English (US)",

series = "Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "132--140",

booktitle = "Proceedings - 4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999",

note = "4th IEEE International Symposium on High-Assurance Systems Engineering, HASE 1999 ; Conference date: 17-11-1999 Through 19-11-1999",

}

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 -

Identifying domain axioms using binary decision diagrams

Abstract

Publication series

Other

Publisher link

Find It

Other files and links

Fingerprint

Cite this