SOFAT

A Scenario Oracle and Formal Analysis Toolbox

Sofat  is a formal toolbox for manipulation of scenarios. SOFAT was registered at the APP (Agence pour la Protection des Programmes) in 2003 with number  DDN.FR.001.080027.000.S.P.2003.00.10600
 

Downloads

Version 4.0: This is a non documented version of SOFAT. It includes all documented functionalities of SOFATV3, plus a diagnosis tool. Documentation on diagnosis techniques from HMSCs can be found here.

Some examples of HMSCS can be downloaded here.

Former releases

 version 1.1 of SOFAT available  here

03/02/2004 :  Version 1.2 availaible : Some bugs were corrected.

Version 2: Not distributed.

Version 3.0: One of the features of this version is a interface which is more functional and easy to use. The simulation feature available in version 2 is disabled.

Installation

Before using SOFAT, you will need a version of the JDK greater than 1.2.
It can be found on  SUN's website : http://java.sun.com/products/jdk/1.2/

You will also need a version of DOT, distributed with the graphviz package. It can be found here.
 

Licence

SOFAT is a free software, but is protected by a licence. The terms of the licence can be found [here].

Bugs

despite our careful testing, SOFAT may still contain bugs.
You can help us improving the tool, and send a mail to : loic(nospam).helouet (nospam) @ irisa.fr

Publications and presentations

- Fast presentation of SOFAT [PS] (Version 1.2)
- Slides describing the principles of SOFAT [ppt] (Version 1.2)
- Simulation : the principles of the simulation algorithm. a paper published in SDL'99 [ps]
- A description of MSCs semantics using event structures [ps]

User Manual

- Version 1.2 Manual [DOC] (Still very incomplete)
- Version 3.0 Manual Version3.0 Manual (PDF)
 

Some snapshots of the software

Fig. 2 Graphical representation of a HMSC in Sofat

Fig. 3 Graphical representation of a BMSC in Sofat

Last Modification : 12/09/2008