Edinburgh Concurrency Workbench Summary
The Edinburgh Concurrency Workbench (CWB) is an automated tool which caters
for the manipulation and analysis of concurrent systems. In particular, the
CWB allows for various equivalence, preorder and model checking using a
variety of different process semantics.
For example, with the CWB it is possible to:
- define behaviours given either in an extended version of CCS
or in SCCS, and perform various analyses on these behaviours, such
as analysing the state space of a given process, or checking various
semantic equivalences and preorders;
- define propositions in a powerful modal logic and check whether a
given process satisfies a specification formulated in this logic;
- play Stirling-style model-checking games to understand why a process
does or does not satisfy a formula;
- derive automatically logical formulae which distinguish nonequivalent
processes;
- interactively simulate the behaviour of an agent, thus guiding it
through its state space in a controlled fashion.
For more detail, see the Documentation page.
Back to CWB home page