Subscribe
Issue No.09 - September (1990 vol.16)
pp: 993-1004
ABSTRACT
<p>How a mechanized tool for reasoning about CSP (communicating sequential processes) can be developed by customizing an existing general-purpose theorem prover based on higher-order logic is described. How the trace semantics of CSP operators can be mechanized in higher-order logic is investigated, and how the laws associated with these operators can be proved from their semantic definitions is shown. The resulting system is one in which natural-deduction style proofs can be conducted using the standard CSP laws.</p>
INDEX TERMS
mechanising CSP trace theory; higher order logic; communicating sequential processes; general-purpose theorem prover; formal logic; formal specification; theorem proving.
CITATION
A.J. Camilleri, "Mechanizing CSP Trace Theory in Higher Order Logic", IEEE Transactions on Software Engineering, vol.16, no. 9, pp. 993-1004, September 1990, doi:10.1109/32.58786