The Underlying Semantics of Transition Systems

This paper formalizes an operational semantics for the transition system model of concurrency and presents proof rules justified by that formalization. The operational semantics and the proofs rules have been mechanically verified on an automated theorem prover, and have been used to mechanically verify the correctness of a message passing solution to the n-processor mutual exclusion problem. 3 1. Introduction The transition system model is the interpretation underlying many proof systems for the verification of concurrent programs. Such proof systems contain proof rules which are justified by the interpretation. Typically, these proof rules are demonstrated to be complete with respect to interesting properties of the interpretation. In this paper, we define an operational semantics that formalizes an interpretation of the transition system model. We then show how this operational semantics can be used as the basis of a proof system for concurrent programs and how this proof system ..