The Concurrency Workbench of the New Century (CWB-NC) provides support for the automated verification of concurrent software systems. The tool allows the user to write a description of the system at hand in one of several design languages (CCS, CSP, LOTOS, PCCS, SCCS, TCCS). Furthermore it supports a variety of automated verification and analysis techniques to check whether the system adheres to its specifications.
Among the verification and analysis techniques are:
- Behavioral-Relation-Based Verification
- Temporal-Logic-Based Verification
- Interactive Simulation
- Reachability analysis