Please note: These pages are work in progress!
soter
- Safety checker fOr The ERlang language!
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.
Soter normally goes through three phases:
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:
0
.10
.1
.12
; if one of the calls to BFC does not terminate within the time-limit then Soter will terminate with exit code 13
.input is assumed to be in CoreErlang
do not apply simplification of ACS
use a Peano encoding of positive integers (use with care)
the name of the function representing the entry point of the program; it must be of arity 0
. The default is `main'
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.
show statistics
Loud verbosity
Quiet verbosity
Reserved for future use
attempt to prove absence of any error
attempt to prove absence of assertion violations
attempt to prove absence of `error' exceptions
tells Soter to prove the specified property. See soter(7) for syntax.
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.
specifies a depth for the data abstraction
specifies a depth for the message abstraction
timeout for the CFA in seconds (no timeout if <= 0)
timeout for the BFC verification in seconds (no timeout if <= 0)
Display help message
Print version information
The Erlang module supplied as input should follow these guidelines:
-module(modname)
.main()
function which acts as entry point. Entry points with free variables are not supported but can be simulated via non-deterministic choice (see soter(7))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.
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
myfile.ir
myfile.cfa
myfile.dot
myfile.bfc
myfile.simpl.*
myfile.stats
myfile.results
Soter deals with a `pure' core fragment of the Erlang language. See soter(7) for details.
Soter can be very slow for big inputs. Use with care.
© Oxford University 2012
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)