Homepage: http://www.daxc.de/eth
This tool can be used to accelerate the automata-based approach of finte-state model checking when the specification is a boolean combination of safety properties.
In the automata-based approach for finite-state model checking, the system model as well as the temporal-logic specification for bad system bahaviour are represented by nondeterministic Büchi automata (NBAs). That is, the language of the system automaton is the set of system traces and the language of the specification automaton is the set of bad traces. The system model satisfies the specification if there is no bad system trace, i.e., the synchronous product of the system automaton and the specification automaton does not contain any trace.
To accelerate the search for a bad trace in the product automaton, several techniques have been established to reduces the size of the specification automaton and to make its transition graph "more deterministic". For a specification that is a boolean combination of safety properties, we can translate the NBA into a minimal weak deterministic Büchi automaton (WDBA). Experiments have shown that in general, the minimal WDBAs are smaller than the NBAs and that using WDBAs instead of NBAs, model checking needs less computation time and less memory.
The WDBA tool reads the NBA for bad traces and the NBA for good traces given as SPIN neverclaims. The second NBA is needed to check whether the first NBA represents a specification that is a boolean combination of safety properties. The tool transforms the first NBA into an WDBA and outputs the automaton as SPIN neverclaim.
See also the paper "Mechanizing the Powerset Construction for Restricted Classes of omega-Automata" available at http://www.inf.ethz.ch/personal/daxc/index.html for detailed information.
The current version is beta release only and no warranty can be given. The WDBA tool is distributed under the BSD license. You will need an OCaml (http://caml.inria.fr) to compile the source code.
Download the newest version of the WDBA tool wdba_2009-03-03.tar.gz: [ DOWNLOAD ]