A Comparison of Simulation Techniques and Algebraic Techniques for Verifying Concurrent Systems

Appears: Journal of Formal Aspects of Computing Science, 7(3):231-265, 1995.

Also: An extended abstract appears in Proceedings of the Second North American Process Algebra Workshop, Cornell University, NY, 1993. Abstract also available as Technical Memo MIT/LCS/TM-499.

Abstract: Simulation-based assertional techniques and process algebraic techniques are two of the major methods that have been proposed for the verification of concurrent and distributed systems. It is shown how each of these techniques can be applied to the task of verifying systems described as input/output automata; both safety and liveness properties are considered. A small but typical circuit is verified in both of these ways, first using forward simulations, an execution correspondence lemma, and a simple fairness argument, and second using deductions within the process algebra DIOA for I/O automata. An extended evaluation and comparison of the two methods is given.

Download the full paper from the publisher.

Download the Technical Memo with the extended abstract.