|Title||Using Model Checking to Generate Tests from Requirements Specifications|
|Publication Type||Conference Paper|
|Year of Publication||1999|
|Authors||Gargantini, A., and C. L. Heitmeyer|
|Conference Name||Joint 7th Eur. Software Engineering Conf. and 7th ACM SIGSOFT Intern. Symp. on Foundations of Software Eng. (ESEC/FSE99)|
|Conference Location||Toulouse, France|
Recently, many formal methods, such as the SCR (Software Cost Reduction) requirements method, have been proposed for improving the quality of software specifications. Although improved specifications are valuable, the ultimate objective of software development is to produce software that satisfies its requirements. To evaluate the correctness of a software implementation, one can apply black-box testing to determine whether the implementation, given a sequence of system inputs, produces the correct system outputs. This paper describes a specification-based method for constructing a suite of "test sequences", where a test sequence is a sequence of inputs and outputs for testing a software implementation. The test sequences are derived from a tabular SCR requirements specification containing diverse data types, i.e., integer, boolean, and enumerated types. From the functions defined in the SCR specification, the method forms a collection of predicates called "branches", which cover all possible software behaviors described by the specification. Based on these predicates, the method then derives a suite of test sequences by using a model checker's ability to construct counterexamples. The paper presents the results of applying our method to four specifications, including a sizable component of a contractor specification of a real system.
|NRL Publication Release Number|| |