The Meije Verification Toolset
for LOTOS verification
The Meije Verification Toolset is connected to the Lotosphere
environment and can be used for Lotos programs. It contains tools for:
-
building finite transition systems and minimizing them along
various bisimulation equivalences;
-
abstracting them with a notion of abstract actions;
-
proving equivalences;
-
displaying the computed automata graphically.
The tools are concerned with implicit and explicit representations of
automata and with compositional computations.
Further information may be obtained on the
WWW
.
The Minilite Lotosphere environment for Lotos is also distributed.