Interaction between concurrently executing processes gives rise to special considerations that do not apply to sequential processes. Program correctness needs to be considered with respect to safety properties and liveness properties. This paper considers these issues in the context of autonomous error-recovery strategies on the Galileo spacecraft.

Safety properties arise from timing constraints (which prevent a given command being issued within t seconds of some other command); precedence constraints (which ensure that a given command occurs only after some other command has been issued); and data consistency constraints (which restrict simultaneous access to data by concurrent processes). Data consistency may be ensured by constraining the sequencing of the relevant access operations, so data consistency constraints are modeled as precedence constraints. Since precedence constraints guarantee, on the issuing of a given command, that some other command has been issued, they determine the liveness property of the precedent command.

The paper presents a tool for detecting violations of a set of constraints, expressed as a constraint graph. The commands are nodes of the graph, and constraints (relating two commands) are represented by edges. Interacting processes may, in general, yield event interleavings of arbitrary complexity, but, the authors claim, the control structure of spacecraft processes is sufficiently simple that it lends itself to analysis by the constraints checker. The algorithm for the constraints checker is described, and an example (with 40 constraint edges) is presented.

This work is a useful contribution to the verification of concurrent systems. The existence of this tool should enable improved analyses of concurrent systems, especially if it can be generalized to handle a greater variety of constraints.