Using model checking to generate tests from requirements specifications

TLDR

Formal methods such as SCR aim to improve software specifications, yet the ultimate goal remains producing software that satisfies its requirements, which can be evaluated through black‑box testing. This paper proposes a specification‑based approach to generate test sequences from SCR requirements. The method extracts predicates (branches) from the SCR specification and employs a model checker to generate counterexamples that become test sequences covering all specified behaviors. Applying the method to four specifications, including a large component of a real contractor system, demonstrated its practical applicability.

Abstract

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.