PROFUNDIS: Proofs of Functionality for Mobile Distributed Systems
[ Overview | Meetings | Visits | Events | Publications | Tools | Internal information ]
Links to prototype tools developed in the PROFUNDIS project:
verification web is the prototype of the distributed
tool architecture of the project. Both MIHDA, STA, and the
MWB (see below) are, to some degree, integrated in this.
is a framework (API and toolkit) to minimize (through a
partition refinement algorithm) classes of automata-like
specifications. In the current implementation, HD-reducer
handles standard finite state automata and
HD-automata. HD-reducer is implemented in OCAML and supports
early semantics of pi-calculus (finite control) agents.
- MWB: the Mobility Workbench is a tool for manipulating and analyzing
mobile concurrent systems described in the pi-calculus. The functionality includes checking open bisimulation equivalence, and model checking a variant of the modal mu-calculus.
- STA: (Symbolic Trace Analyzer), a tool for formal analysis of security protocols.
- TRUST: the symbolic protocol analyser by Vincent Vanackčre
- Spatial Logic Model Checker: a tool that allows the user to automatically verify behavioral and spatial properties of distributed concurrent systems expressed in the pi-calculus.
- GcPAN: an efficient abstract machine for Safe Ambients
Web page: Björn Victor, latest update Tue, 05-Apr-2005 14:09 MEST