Reactis has its roots in several research tools developed by RSI personnel that put advanced reactive system design automation into practice. We briefly survey these tools here; for more information we provide links to the home pages of these tools.
The Concurrency Workbench of the New Century
The Concurrency Workbench of the New Century is an easily customized tool for verifying systems written in different process algebras. A key feature of the CWB-NC is its modular design and concomitant flexibility. The tool strictly segregates modeling-language-specific routines (parsers, unparsers, semantic functions) from the verification procedures, which work at the level of state machines and are hence independent of the specific notation from which the state machines are derived. The analytical facilities of the system are in turn built around generic algorithms for model checking and equivalence checking. The former checks whether system descriptions satisfy system formulas in the mu-calculus, a low-level but very expressive temporal logic into which other temporal logics may be efficiently translated. The equivalence checker combines an algorithm for computing bisimulation equivalence with state-machine transformations to provide a uniform framework for calculating a variety of different behavioral equivalences.
The Workbench has been acquired by over 600 sites around the world (25 countries on five continents, at last count) and has been used successfully on a variety of case studies. The public distribution of the most recent release (version 1.2) of the tool may be found at the link provided above.
The Process Algebra Compiler
The Process Algebra Compiler (PAC) is a front-end generator for verification tools such as the CWB-NC. Given high-level descriptions of a modeling language's syntax and its operational semantics, the PAC produces syntactic routines and functions for computing the semantics of programs in the algebra. Use of the PAC greatly simplifies the task of adapting verification tools to the analysis of systems described in different languages; it may therefore be used to achieve source-level compatibility between different verification tools. The generated front-ends also significantly out-perform hand-crafted code contained in old versions of the CWB, owing to two optimizations the PAC includes in the code it produces.
- Transition caching. When execution steps for a given process-algebra term are calculated, they are saved and re-used as necessary.
- Tree flattening. Terms are represented as pointers into tables rather than as abstract syntax trees. This permits efficient syntactic equality checking and hashing on terms.
The Concurrency Factory
The Concurrency Factory is an integrated environment for the modeling and verification of concurrent systems. Like the CWB-NC, the Concurrency Factory uses process algebra as the theoretical basis for its formal modeling notation and model checking as its primary validation technique.
The Concurrency Factory's model checker is a local model checker: given a system S and formula f, it explores only that portion of S's state space needed to determine if S satisfies f. Empirical studies have shown that local model checking can yield significant efficiency gains in practice. The Factory's model checker also implements a new partial-order reduction technique, which further reduces the size of the state space that needs to be explored.
To ease the task of developing system models, the tool supports a structured, graphical co-ordination language that may be used to ``glue together'' the designs of system components given in a textual or graphical notation. Experience has shown that graphical syntax is typically better for conveying the architectural aspects of a specification while textual syntax is better for specifying complex data and control logic.
Finally, the Factory supports automatic code generation. Verified designs may be automatically translated into Java or Ada 95 code. In the case of Ada, the user may specify code generation for a single-processor execution platform or a distributed, multi-node platform.
Salsa
Salsa is an invariant checker for models specified in SAL (SCR Abstract Language). To establish a formula as an invariant, Salsa carries out an induction proof that utilizes tightly integrated decision procedures (currently a combination of binary-decision-diagram (BDD) algorithms and a constraint solver for integer linear arithmetic) for discharging the verification conditions.
Unlike most other inductive provers, Salsa works in a totally automatic fashion. Its user interface mimics that of a model checker: given a formula and a model, Salsa either establishes the formula as an invariant of the model or provides a counter example. In either case, the algorithm will terminate. Unlike model checkers, Salsa returns only a state-pair as a counterexample (the states before and after the state that is reached where the invariant does not hold) rather than an entire execution sequence. Also, due to the incompleteness of induction, users must validate the counterexamples.
The use of induction enables Salsa to combat the state-explosion problem that plagues model checkers: it can handle specifications whose state spaces are too large for model checkers to analyze. Also, unlike general-purpose theorem provers, Salsa concentrates on a single task and gains efficiency by employing a set of optimized heuristics.