System design
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. 

 

[Home][Top level Commands][Simulator Commands][Download]