Title :
Mechanizing CSP trace theory in higher order logic
Author :
Camilleri, Albert John
Author_Institution :
Hewlett-Packard Lab., Stoke Gifford, UK
fDate :
9/1/1990 12:00:00 AM
Abstract :
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
Keywords :
formal logic; formal specification; theorem proving; communicating sequential processes; general-purpose theorem prover; higher order logic; mechanising CSP trace theory; Algebra; Concurrent computing; Formal verification; Helium; Humans; Information systems; Logic functions; System recovery;
Journal_Title :
Software Engineering, IEEE Transactions on
