Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench
The modelling of delay-insensitive asynchronous circuits in the process calculus CCS is addressed. MUST-testing (rather than bisimulation) is found to support verification both of the property of delay-insensitivity and of design by stepwise refinement. Automated verification is possible with a well-known tool, the Edinburgh Concurrency Workbench. (C) 2003 Elsevier B.V. All rights reserved.
formal methods specification languages formal verification asynchronous logic