PROFUNDIS: Proofs of Functionality for Mobile Distributed Systems

[ Overview | Meetings | Visits | Events | Publications | Tools | Internal information ]

Software tools

Links to prototype tools developed in the PROFUNDIS project:

• Profundis 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.
• HD-Reducer 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