Enforcing Concurrent Temporal Behaviors

AbstractThe outcome of verifying software is often a 'counterexample', i.e., a listing of the actions and states of a behavior not satisfying the specification. In order to understand the reason for the failure it is often required to test such an execution against the actual code. In this way we also find out whether we have a genuine error or a “false negative”. Due to nondeterminism in concurrent code, recovering an erroneous behavior on the actual program is not guaranteed even if no abstraction was made and we start the execution with the prescribed initial state. Testers are faced with a similar problem when they have to show that a suspicious scenario can actually be executed. Such a scenario may involve some intricate scheduling and thus be illusive to demonstrate. We describe here a program transformation that translates a program in such a way that it can be verified and then reverse transformed for testing a suspicious behavior. Since the transformation implies changes to the original code, we strive to minimize its effect on the original program