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 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''

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 North Carolina (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.

As stated in the above, one of the main features of the CWB-NC is its flexibility; in particular, users should be able to 1) add new equivalences and preorders, and 2) alter the language used for defining systems. In support of the first goal, the design of the CWB-NC uses generic preorder/equivalence-checking algorithms in conjunction with system and formula transformations in order to compute equivalences and preorders. To illustrate the approach, we explain how the tool calculates its response to the command eq -Smust Spec ABP mentioned in the previous section.

1. Spec and ABP are ``compiled'' into automata.
2. These automata are transformed into a type of deterministic automata.
3. The transformed automata are fed into a generic equivalence checker, which calculates whether or not the two automata are bisimulation equivalent. If they are not equivalent, the checker produces a formula in a special logic that distinguishes the two automata.
4. If a formula is produced, a formula transformer converts it into a test, which is then returned to the user.

This general scheme is robust: numerous equivalences may be computed, and relevant diagnostic information generated, using appropriate transformations in tandem with bisimulation equivalence. Consequently, to add an equivalence relation to the CWB-NC, one need only define an appropriate process transformation and, if diagnostic information is desired, a formula transformation. A similar scheme is used for preorders.

In support of the second goal, all language-specific information has been localized within one module inside the CWB-NC. This module may be thought of as encapsulating the parse trees resulting from processing a user-supplied system description; it exports parsing and unparsing functions, and semantic routines (such as those for calculating single-step transitions), for these trees to the rest of the tool. To change the system description language, then, one need only alter routines in this module. The Process Algebra Compiler greatly eases this task by providing users with a high-level notation in which to define the syntax and (operational) semantics of their languages. Using this tool, front ends for CCS, CSP, Basic Lotos, a version of CCS with priorities, and other languages have been generated for the CWB-NC.

One typical trade-off in system development involves flexibility vs. efficiency: generally speaking, the more a system tries to do, the less efficiently it is able to do it. In our implementation of the CWB-NC we have exploited several ideas to try to minimize the performance impact of the tool's modular design; in particular, heavy use is made of structure sharing and intermediate-result caching. Although a systematic study of the system's performance has yet to be undertaken, our experience so far suggests that it compares favorably with other, more specialized tools.

• The connection phase of the UNI (Version 3.0) protocol used in ATM networks was formalized in CCS and verified. The largest finite-state machine handled in the course of the analysis contained about 60,000 reachable states.
• The timing behavior of an active-structure control system was analyzed. The system was formalized in a real-time variant of CCS and contained in excess of 10^19 states. By minimizing the system in a component-wise manner, however, the analysis was carried to completion.
• The functional behavior of different variations of a railway signaling system was analyzed. The language used to define the system borrowed constructs from several different process algebras, while the system's requirements were specified using mu-calculus formulas.

As future work, we plan to investigate techniques for computing and displaying diagnostic information when systems fail to satisfy temporal formulas. We have also partially implemented on-the-fly versions of the preorder/equivalence-checking routines with a view to comparing the performance of global and on-the-fly algorithms.

R. Cleaveland and S. Sims. "The NCSU Concurrency Workbench." In R. Alur and T. Henzinger, editors, Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 394--397, New Brunswick, NJ, July 1996. Springer-Verlag.

Gives an overview of the CWB-NC (which at one point was called the NCSU Concurrency Workbench).

R. Cleaveland, G. Luettgen, V. Natarajan and S. Sims. "Modeling and verifying distributed systems using priorities: A case study." Software Concepts and Tools 17:50--62, 1996.

Describes a case study conducted using the CWB-NC.

• Steve Sims
• Rance Cleaveland