Please note: These pages are work in progress!

CONTENTS

NAME

soter - Safety checker fOr The ERlang language!

SYNOPSIS

soter [OPTIONS]... FILE

soter --stats module.erl
soter --dump --quiet module.erl

DESCRIPTION

Soter is a program analyser for Erlang modules. It extracts an abstract (approximate sound) model from the source-code of the Erlang module and tries to verify safety properties of it using a powerful model checking back-end (BFC).

The name Soter derives from the Ancient Greek name of the spirit of safety, preservation and deliverance from harm.

Please Note: in order for Soter to work properly you need to have BFC installed in you system and the bfc executable must be in your PATH.

Output meaning:

Soter normally goes through three phases:

  1. Parsing of input Erlang module;
  2. Extraction of the abstract model;
  3. Verification of the properties (using BFC).

If phase 1 or 2 encounter errors, error messages get written to stderr and Soter terminates with exit code 1.

In phase 3, Soter will attempt to verify each of the specified properties in turn. The outcome of such attempts can be one of:

OPTIONS

Input:

-f --fromcore

input is assumed to be in CoreErlang

--no-simpl

do not apply simplification of ACS

--peano

use a Peano encoding of positive integers (use with care)

-m --main=FUN-NAME

the name of the function representing the entry point of the program; it must be of arity 0. The default is `main'

Output:

-d --dump -odir=[DIR]

dump all intermediate results to the specified directory; if no directory is specified, soter will use (and create if non existing) a directory with the name of the module in the directory of the module. The dumped files are described in the Output files section.

-s --stats

show statistics

-v --verbose

Loud verbosity

-q --quiet

Quiet verbosity

--json

Reserved for future use

Verification:

-A --prove-all

attempt to prove absence of any error

-a --prove-assertions

attempt to prove absence of assertion violations

-e --prove-no-error

attempt to prove absence of `error' exceptions

-u --prove --uncoverable=PROP

tells Soter to prove the specified property. See soter(7) for syntax.

--prop[=FILE] --prove-file

tells Soter to prove every property specified in the .prop file. If no file is specified Soter will attempt to read a .prop file with the same basename of the input Erlang module. See soter(7) for syntax.

-D --val-depth=INT

specifies a depth for the data abstraction

-M --msg-depth=INT

specifies a depth for the message abstraction

--ct --cfa-timeout=INT

timeout for the CFA in seconds (no timeout if <= 0)

--bt --bfc-timeout=INT

timeout for the BFC verification in seconds (no timeout if <= 0)

Help:

-? --help

Display help message

-V --version

Print version information

ERLANG INPUT MODULE

The Erlang module supplied as input should follow these guidelines:

Refer to soter(7) for a detailed description of the current restriction on the Erlang programs accepted by Soter.

A tipical Erlang module that can be analysed by Soter looks like the following:

-module(example).
-compile(export_all).

-include_lib("soter.hrl").
-include_lib("grammars.hrl").

-uncoverable("wrong_incipit > 0").

main() ->
    N = ?any_nat(),
    P = spawn(fun()-> f(N) end),
    P ! {hi, self()} ,
    receive
        X -> X
    end.

f(N) ->
    receive
        {hi, P} ->
            P ! {hey, N}
            start_protocol(N, P);
        bla ->
            ?label(wrong_incipit),
            complain(N)
    end.

...

See soter(7) for the full details.

OUTPUT FILES

Suppose FILE = examples/myfile.erl then after running soter on it you will find a new subdirectory of examples/ called myfile containing the following files:

myfile.core
This is the Core Erlang version of myfile.erl
myfile.ir
This is the Intermediate Representation of the program
myfile.cfa
This is the full content of the output of the CFA
myfile.dot
This file (meant to be used with acsview.py) is a Graphviz file showing the generated ACS in graphical form
myfile.bfc
The ACS model translated into the BFC input format. The ids of the local states coincide with the ones displayed in the nodes of the ACS in the dot file
myfile.simpl.*
These files correspond to translations of the ACS after simplification
myfile.stats
This contains a summary of the performance
myfile.results
This contains the results of the verification of each property.

BUGS

Limitations

Soter deals with a `pure' core fragment of the Erlang language. See soter(7) for details.

Reporting Bugs

Email bug reports to

Known Bugs

Soter can be very slow for big inputs. Use with care.

SEE ALSO

BFC is a program by Alexander Kaiser and can be downloaded at http://www.cprover.org/bfc

Details on the syntax for properties can be found at soter(7)