Enforcing concurrent temporal behaviors

Abstract

The outcome of verifying software is often a 'counterexample', i.e., a listing of the actions and states of a behavior not satisfying the specification. The verification is usually done using a model of the software (often also using some abstraction to reduce its complexity) rather than the actual code. In order to understand the reason for the failure manifested by such a counterexample, it is sometimes necessary to test such an execution using 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, enforcing a particular behavior of an actual program is not guaranteed even when one starts the execution with the prescribed initial state. Testers are faced with a similar problem when they have to demonstrate 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 transformation that allows us to repeat a selected execution sequences of concurrent code. Since the transformation implies changes to the original code, we strive to minimize its effect on the original program. © World Scientific Publishing Company.