9309043 Carver Specification-based development provides a rigorous and definitive basis for comparing the intended and actual behavior of a concurrent program. Nondeterministic behavior of concurrent programs creates the following problem during testing: when testing P with input X, a single execution is insufficient to determine the correctness of P with input X. Even if P with input X has been executed successfully many times, it is possible that a future execution of P with input X will produce an incorrect result. To deal with this problem, we force deterministic executions of P according to given synchronization sequences. Test sequences can be selected from P or from its specification. We will investigate how to derive constraints from specifications. Constraints derived from a specification can be compared with the actual constraints derived from source code in order to detect errors. Concurrent programs will be formally specified using process algebras and temporal logic. New techniques and tools will be incorporated into an existing validation environment to support both specification and program-based testing and analysis. ***
