The CWB-NC provides support for automatically answering the verification question: does system sys satisfy specification spec? To implement such a tool, the verification question must be formulated more carefully by fixing the following: 
 

•  a precise notation for defining systems 
•  a precise notation for defining specifications 
•  what it means for a system to satisfy a specification 

 The CWB-NC supports several formulations of the verification question. 

 The simplest type of verification supported by the tool is reachability analysis. Here, as in each type of verification, the first step in using the tool is to write a description of the system at hand in one of the several design languages supported by the CWB-NC. The description is then parsed by the tool and checked for syntactic correctness. The user then gives a logical formula describing a ``bad state'' that the system should never reach. Given such a formula and system description, the CWB-NC explores every possible state the system may reach during execution and checks to see if a bad state is reachable. If a bad state is detected, a description of the execution sequence leading to the state is reported to the user. Many bugs such as deadlock and critical section violations may be found using this approach. 

Reachability analysis is actually a special case of a more general type of verification called model checking. In the model checking approach a system is again described using a design language and a property the system should have is formulated as a logical formula. However, in model checking rather than specifying a ``bad state'' to be searched for among the reachable states of the system, the given formula defines a behavior the system should or should not have as it executes. The logic used for expressing formulas contains temporal operators enabling one to describe how a system behaves as time passes rather than simply a characteristic of the system at a particular point in time. Using such a temporal logic one can state properties such as the following: 

           ``eventually event a will occur''
           ``it is always the case that after an a event the event b eventually occurs'' 

The CWB-NC includes a model checker for determining whether systems satisfy formulas written in an expressive temporal logic, the modal mu-calculus. Many other logics may be efficiently translated into the mu-calculus; therefore, it may serve as the basis for model checking in a variety of different logics. The CWB-NC checks CTL formulas using this approach. 

A third type of verification supported by the CWB-NC involves using a design language for defining both systems and specifications. Here the specification describes a system behavior more abstractly than the system description. A binary relation over terms in the design language is defined such that a system satisfies a specification if the two terms in the design language (the system and specification) are related by the relation (called a behavioral relation). Two basic approaches have been advocated for defining behavioral relations. If a relation R is an equivalence relation (i.e. a relation that is reflexive, symmetric, and transitive), then two terms related by R behave the same according to some criteria. Different relations may be defined to capture different notions of behaving the same. In a second approach R is defined as a preorder (i.e. a relation that is reflexive and transitive) and spec R sys indicates that sys behaves the same or better than spec. Efficient algorithms have been developed for equivalence and preorder checking and routines for performing these types of verification have been implemented in the CWB-NC. The CWB-NC also provides appropriate diagnostic information for explaining why two systems fail to be related by a given semantic equivalence or preorder. 

The design of the system exploits the language-independence of its analysis routines by localizing language-specific procedures (syntactic analyzers, semantic functions) in one module. This enables users to change the system description language of the CWB-NC using the Process Algebra Compiler of New Century (PAC-NC). Using this tool a number of front ends have been implemented to support a number of different design languages including CCS, a version of CCS with priorities, timed CCS, CSP, and Basic Lotos. 

In order to enable the tool to handle large ``real-world'' systems we have also paid great attention to issues of time- and space-efficiency. 

 User Interface

  The CWB-NC supports two user interfaces: one text-based, and hence capable of running on a  variety of different platforms, and the other graphical, and hence easier to use. Each consists of a  ``command loop''; users enter commands either textually or by pushing buttons, and the system calculates and displays the result. To analyze a system, a user first creates a file containing the definition of the system in the language supported by the version of the CWB-NC at hand, invokes the tool, loads the file into the CWB-NC, and executes appropriate commands. 

Commands

In addition to providing a system simulation facility, the CWB-NC can compute a number of behavioral equivalences and preorders and calculate whether or not systems satisfy mu-calculus formulas. The textual interface of the CWB-NC uses a shell-like syntax for commands corresponding to these procedures. For example, the command to check whether systems Spec and ABP are must equivalent is the following: eq -Smust Spec ABP. Here the qualifier for the -S flag indicates which semantic equivalence should be checked; other possible qualifiers include sim (simulation equivalence), obseq (observational equivalence), trace (trace equivalence), and several others. The general command for preorder checking, le, uses the same scheme for specifying which ordering to check. In any case, appropriate diagnostic information is returned to the user when the given systems are found to be unrelated. For example, two systems are must equivalent iff they must pass exactly the same tests (in a precisely defined sense). Thus if Spec and ABP are not must equivalent, there must be a test that distinguishes them; when this is the case the CWB-NC computes such a test and displays it to the user. The CWB-NC includes two model checkers, each of which allow users to specify formulas in a particular subset of the modal mu-calculus; one accepts formulas in the alternation free fragment while the other accepts formulas in the L2 fragment. The system also supports commands for minimizing systems with respect to certain equivalences; this proves to be very useful in fighting state explosion. 

Implementation

The CWB-NC is implemented in SML of New Jersey and consists of approximately 18,000 lines of code.