CWB-NC applications |
| To date the CWB-NC has been applied
to the analysis of several different systems, including the following.
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 and GCTL* formulas. The functional behavior of the SCSI-2 Bus Protocol was also analyzed; the behavior was defined in a version of CCS with action priorities, and properties specified in both the mu-calculus and GCTL*. 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. |