| Abstract: | ![]()
The validity of the first (formal) model of a system to be developed is crucial for the whole development process. Systematically checking this validity helps avoid costs that could arise if it were discovered too late that the system does not satisfy the customer's needs and expectations. This paper addresses how to validate synchronous reactive programs using the technique of systematic testing. Testing reactive systems differs from testing sequential systems: instead of checking simple pairs of inputs and outputs, sequences of inputs and outputs have to be checked. Thus, testing cannot be based on a simple function model, mapping input values onto output values nor on a control flow graph model (where a path from the start node to the final node represents one execution through the represented program). The model widely used instead is that of a finite-state machine. A systematic testing approach is presented that is both effective and efficient for validating reactive systems. It uses an additional specification based on a finite-state machine model. The approach is demonstrated for the well-known lift example. It is shown how to use the specification for carefully choosing a set of test criteria that address different types of fault; a procedure for selecting test cases and test data that satisfy the chosen criteria is presented. |
