Sequence-based software specification of deterministic systems

Specification of software under the box structure method requires a complete, consistent, and traceably-correct description of behavior solely in terms of external stimuli and responses. Such a specification, also called a black box, can be derived from the requirements through straightforward, systematic enumeration of all stimulus sequences. Enumeration is made manageable by the application of techniques for controlling the growth of this inherently combinatorial process, and specifications at different levels of abstraction may be combined to refine a black box specification. This work presents a unifying framework for development of specifications and testing models, and the focus on requirements traceability provides an explicit means to manage requirements change.