Download

This software is released under CeCILL-B license (similar to BSD, without copyleft, cf LICENSE.txt) with Copyright 2015 CNRS-LAAS. The authors are: Mathilde Machin, Fanny Dufossé, Lola Masson
The framework is constituted of the modeling template, an initialisation program and the synthesis tool. See readme and examples in the archive.

This set of tools is intended to synthesis high-level safety requirement for critical systems, with the concern not to restrict the system functionality.

Tested under Ubuntu (XUbuntu 14.04)

1. Install NuSMV (tested with 2.5.4)
    NuSMV is available through some package managers,
    otherwise
    Download NuSMV
    Add NuSMV folder to the PATH, in .profile

2. Install smof
    2.0 Download smof for the website and unzip it
    2.1 Set the environment variable HOME_SMOF. For this, write in the in .profile file the following line :
                  export HOME_SMOF="/path/to/the/folder/smof"
          and then Reboot (a source .profile is not sufficient)
    2.2 Compile (requires only C, C++ standard libraries and gcc)
        % cd smof/src
        % make

    2.3 Configure the synthesis
        In the folder smof/rsc/, the file conf should be present. The main parameters of the configuration are:
            - selectivity of the synthesis (completeness and minimality), which defines the desired solution set
            - level of verbosity
            - the last parameter to make compatible NuSMV and SRS (depends on your NuSMV installation)
        By default, the configuration is the following: the synthesis will provide only minimal solutions, with a maximu of 15 parallel threads during computation, using NuSMV without Minisat installed

3. Edit an example 

In order to run a synthesis two files are required : a smv and a rsm files. An example is provided in the smof/example folder. You can edit the model in the .smv file (from example.smv) and the associated rsm file (see also example.rsm) which describes the interventions and variables of the example:

            nb of intervention
            name_interv_1
            ...
            name_interv_m
            nb of variables
            name_var_1 max_value_1
            ...
            name_var_n max_value_n

    
In case of unexpected behavior, check the consistency of .rsm and .smv
The .smv file is not modified in 4. A. and B.

4. Launch the initialisation program
(for the files example.smv and example.rsm)
% cd smof
% ./smof_init example/example

That generates the files in the example folder:
    example.auto.smv (your model example.smv with the end of the template)
    example.interact (script for the interactive method (former version))
    and the files .A* for the automatic method (current version)
     example.Awarn (number of non-cata states, number and set of warning states)
     example.Areach (NuSMV script to check reduced permissiveness, ie reachability and universal reachability)
     example.Ac_reach (NuSMV script to check continuous reachbility)

5. Launch the synthesis program
% ./smof_exec example/example
Results are in example.res (strategies are not guranteed to be minimal) or respp (only minimal strategies) (Depends of the completeness-minimality chosen in rsc/conf)

Customisation of generated permissiveness and validity properties can be done in .auto.smv (but will be erased by executing ./smof_init)


*****************
* Some warnings *
*****************

1) The paths are statically allocated. Avoid very long names (ok up to 240 characters for the argument of .exe). For instance example.smv can be replaced by ../../folder/model.smv
2) Intervention names are limited to 10 characters.
3) The number of interventions (e.g., as declared in rsm) is limited to sizeof(int)
4) (for verbosity!=0) The sum of the cut nodes and the generated strategy is equal and a little less than the total number of node of the tree. The potential discrepancy is due to some leaves that are not generates for optimization issues.
5) If the model is modified (even without required .rsm modification), the initialisation should be re-run.
Initialisation computes cata and warning states. Warning states are typically modified if a constraint is added to the model.
If you have modified permissiveness requirements (in .auto.smv), the modification will be lost by rerunning initialisation. Save modifications before.
5) Modification of permissiveness requirements are done by replacing LiveProp() by LiveProp_Uni(), LiveProp_Simple() (or even no module at all).
For instance,if you replace
live_0: LiveProp(...)
by
live_0: LiveProp_Simple(...)
You have to remove from
- .Ac_reach, the line "check_ctlspec -P live_0.uni_c_reach"
- .Areach, the line "check_ctlspec -P live_0.uni_reach"
- .interact, in alias perm, "check_ctlspec -P live_0.reach ;check_ctlspec -P live_0.uni_reach "
6) The smv file must end with a carriage return. In case of error "nb_interv undefined", please check it.
7) If errors happen or results are unexpected, please check that .rsm is consistent with .smv
8) To debug, if smof_exec exits, run
% NuSMV -source rsc/script_fsm rsc_temp/to_proc.smv
(replacing script_fsm by script_safe, script_valid, model.Areach), or
% NuSMV -source rsc/script_safe rsc_temp/to_proc_sl*.smv
It should make a NuSMV message appear.
Do it for each to_proc_sl*.smv

 

***************
* Using NUSMV *
***************

- Event 0 not found   ->   Problem in the NuSMV script
- no space in the alias command (at least in the constraints declared with -c)
- do not use TRANS for constraints without any next()