Integrating formal methods and testing for concurrent programs

An abstract program is a formal specification that models the valid behavior of a concurrent program without describing particular implementation mechanisms that achieve this behavior. In this paper, we address the problem of how to select event sequences from an abstract program to test its concrete implementation. Sequencing constraints make explicit certain types of required properties that are expressed only implicitly by the abstract program itself. The sequencing constraints derived from an abstract program can be used to guide the selection of event sequences during testing: sequences are selected to check the implementation for conformance to the required properties. We describe a constraint notation called CSPE and formally define CSPE constraints in the propositional modal μ-calculus. CSPE constraints can be automatically derived from abstract CCS and Lotos programs. Test sequences can be generated to cover the constraints. We describe a test sequence generation tool that can be used to partially automate this process. The results of an empirical study of constraint-based testing are reported