Specification-based test sequence selection and mapping techniques for concurrent programs

Specification-based testing of concurrent programs requires that test sequences be selected from the specification and mapped to the implementation. In this dissertation, we present new test sequence selection and mapping techniques. Our selection technique requires the use of CSPE (Constraints on Succeeding and Preceding Events) sequencing constraints. CSPE constraints specify restrictions on the allowed sequences of synchronization events, and can be automatically derived from finite-state machine specifications. We show how CSPE constraints support an incremental testing strategy. During incremental testing, the specification is partitioned into two or more components and test sequences are selected from each component separately. Using existing incremental analysis techniques, components can be reduced into smaller but observationally equivalent components. This combination of incremental testing and analysis helps alleviate the state explosion problem when tests are generated from finite state machines. We describe how the structure of a constraint-oriented Lotos specification can be used to provide guidance for the partitioning process during incremental testing.;The test sequences selected from Lotos specifications must be mapped into concrete sequences of the implementation. Our mapping technique maps between test sequences for Lotos and Ada programs. This mapping technique allows us to build tools that partially automate the mapping of specification-based test sequences to implementation-based test sequences.;Finally, we report the results of an empirical study based on the Sliding Window Protocol. We generated test sequences using our incremental test selection technique and measured their effectiveness using the mutation adequacy criterion. The results of our empirical study indicate that our test selection technique is effective for detecting errors.