Verifying Concurrent Processes Using Temporal Logic

Concurrent processes can exhibit extremely complicated behavior, and neither informal reasoning nor testing is reliable enough to establish their correctness. In this thesis, we develop a new technique for the verification of parallel programs. The technique is stated in terms of axioms and inference rules, and it is used to prove safety and liveness properties of parallel programs.
Safety properties are assertions that must be satisfied by the system state at all times; they are analogous to partial correctness. Liveness properties refer to events that will occur in the future, such as program termination or the eventual receipt of a message. In addition to the formal proof rules, we present several heuristics to aid in the preparation of correctness proofs.
We model a parallel program as a set of interacting modules (processes and monitors), and we exploit this modularity in the verification process. First we prove properties of the low-level modules directly from their code. We then combine the specifications of the low-level modules to prove properties of higher-level modules, without again referring to the code. Eventually, we prove properties of the entire program.