Using formal methods to serialize synchronization events

Abstract

One of the difficulties in testing concurrent systems comes from the fact that executions with internal nondeterministic choices make the testing procedure non-repeatable. A natural solution is to artificially enforce and direct the execution to take the desired path so that a test can be reproduced. With a reproducible testing technique, we use a set of test scenarios which consist of pairs of test cases and path constraints, the latter expressing the ordering among certain interesting events during the execution. We consider the automated generation of significant sets of path constraints with a given test case, and we are interested in those sets of path constraints that reflect the possible serializations upon synchronization events during the executions of different processes in the program. Here we present our study on exploring formal engineering methods to generate path constraints when the synchronization events are governed by monitors. © Springer-Verlag 2003.