ProFuN Tools

A visual tool for reliable wireless sensor network application development and maintenance.

Public preview: http://rabbit.it.uu.se:12000/profun/

Documentation: http://parapluu.github.io/profun/

Release of the source code is coming!

Psi-calculi workbench is a parametric tool for concurrent system verification and in particular WSN like networks. It is based on the process calculi formalism and features execution and equivalence checking modules.

The Property-Based Testing Framework for Sensor Networks provides a framework that enables property-based testing of of sensor network applications.

MPass can decide bounded-phase reachability for message passing programs. Each communicating process composing the network can alternate between sending and receiving phases a bounded number of times. Channels composing the network can be of three different semantics: lossy, stuttering or unordered, i.e. messages in the channels can be, respectively, lost, duplicated or re-arranged. MPass efficiently and uniformly reduces the bounded-phase reachability problem into the satisfiability of quantifier-free Presburger formula for each of the above mentioned semantics, thus allowing to leverage the power of SMT solvers.

TBA