TY - JOUR
T1 - Completeness and consistency analysis of state-based requirements
AU - Heimdahl, Mats P E
AU - Leveson, Nancy G.
PY - 1995
Y1 - 1995
N2 - This paper describes methods for automatically analyzing formal, state-based requirements specifications for completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. State space explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e, instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.
AB - This paper describes methods for automatically analyzing formal, state-based requirements specifications for completeness and consistency. The approach uses a low-level functional formalism, simplifying the analysis process. State space explosion problems are eliminated by applying the analysis at a high level of abstraction; i.e, instead of generating a reachability graph for analysis, the analysis is performed directly on the model. The method scales up to large systems by decomposing the specification into smaller, analyzable parts and then using functional composition rules to ensure that verified properties hold for the entire specification. The analysis algorithms and tools have been validated on TCAS II, a complex, airborne, collision-avoidance system required on all commercial aircraft with more than 30 passengers that fly in U.S. airspace.
UR - http://www.scopus.com/inward/record.url?scp=0029190321&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0029190321&partnerID=8YFLogxK
U2 - 10.1145/225014.225015
DO - 10.1145/225014.225015
M3 - Conference article
AN - SCOPUS:0029190321
SN - 0270-5257
SP - 3
EP - 14
JO - Proceedings - International Conference on Software Engineering
JF - Proceedings - International Conference on Software Engineering
T2 - Proceedings of the 1995 IEEE 17th International Conference on Software Engineering
Y2 - 24 April 1995 through 28 April 1995
ER -