Commit 7da35418 authored by Yliès Falcone's avatar Yliès Falcone
Browse files

Add README.md

parents
//////////////////////////////////////////////////////////////////////////////
// DecentMon: an OCaml benchmark for decentralised monitoring of LTL formulae
//////////////////////////////////////////////////////////////////////////////
Current Version 1.1.
-----------------
1. Description: |
-----------------
DecenMon is an OCaml Benchmark for Decentralized Monitoring of LTL formulae. For a full description of the underlying algorithms and principles, we refer the reader to the associated submission to RV 2011.
DecentMon takes as input:
* some LTL formulae to be monitored or some LTL Specification patterns (see the Specification Patterns Website);
* some traces against the formulae are monitored;
an architecture given by a distributed alphabet indicating how components are organised and distributed in the system.
Note that the two first inputs are not mandatory. One can simply indicate a size for a formula that will be automatically generated. Similarly, a size can be indicated for a trace to be automatically generated.
DecentMon then outputs:
* verdicts for the monitored formulae against the input traces;
* some monitoring statistics such as the number of messages exchanged by the local monitors and the length of the trace needed to reach a verdict.
LTL formulae are analysed in two different modes:
a) by using the decentralised approach described above (i.e., each trace is read by a separate monitor), and
b) by merging the traces to a single, global trace and then using a “central monitor” for the formula (i.e., all local monitors send their respective events to the central monitor who makes the decisions regarding the trace).
-----------------
2. Requirements |
-----------------
MANDATORY:
- An OCaml environment and compiler (ocamlc, ocamlopt).
- Ocaml's preprocessor [camlp4]. It can be installed smoothly on Linux and Mac OS X.
OPTIONAL:
- GNU Make
- ocamlweb to generate automatically the documentation.
-----------------
3. Installation |
-----------------
If you have GNU Make available on your machine, a Makefile is provided to ease the installation. Please follow the following steps:
1/ Unzip the distribution in some directory of your choice, e.g., /home/you/DECENTMON.
2/ Goto the directory where the sources have been extracted.
3/ Either:
a) type "make decentmon": it will generate the benchmark in native binary code
b) type "make decentmon_nonat": it will generate a bytecode executable
Prefer option a) if ocamlopt is available on your machine (the benchmark will run faster).
If you don't have GNU Make installed on your machine, please follow first steps 1/ and 2/, and then type:
a) for native code generation:
ocamlopt -I +camlp4 -pp camlp4of.opt types.ml enum.mli enum.ml extString.mli extString.ml IO.mli IO.ml std.mli std.ml ltl.ml ltl_parser.ml ltl_generator.ml progression.ml trace.ml d_progression.ml trace_parser.ml alphabet_parser.ml
b) for bytecode generation:
ocamlc -I +camlp4 -pp camlp4of.opt types.ml enum.mli enum.ml extString.mli extString.ml IO.mli IO.ml std.mli std.ml ltl.ml ltl_parser.ml ltl_generator.ml progression.ml trace.ml d_progression.ml trace_parser.ml alphabet_parser.ml
Installation will generate an executable file named "decentmon".
-----------------------
4. Running DecentMon |
-----------------------
To run the benchmark, it is simply needed to run the executable file "decentmon" with appropriate options.
Two kinds of benchmarks are implemented for now. Options required for both kinds are described below.
-- Benchmarking randomly generated LTL formulae
In this benchmark, one indicates either a specific size for the formulae or a maximum size for the formulae to be tested. Those cases correspond to options:
-sf [integer>0] to indicate a specific size,
-msf [integer>0] to indicate a maximum size.
In that later case, DecentMon will run benchmarks for each formula size from 1 to the desired size. Note that the size of formulae is measured in DecentMon in terms of operator entailment inside the formula. This choice, made after some experiments, reflects the intuitive idea that decentralized monitoring becomes heavier when operator entailment grows (instead of the number of symbols, for example).
Then several other options are mandatory:
-n [integer>0] indicates the number of formulae to be monitored for each formula size,
-st [integer>0] indicates the size of the trace against which formulae will be monitored,
-dalpha [string_representation_of_a_distributed_alphabet] indicates the distributed alphabet to consider during the benchmark (See Section input formats).
-- Benchmark for LTL specification patterns
In this benchmark, one indicates one or several LTL specification patterns to be tested (see the Specification pattern Website: http://patterns.projects.cis.ksu.edu/). For convenience, the various kinds of formulae for each LTL specification patterns are recalled in Appendix B. The options used to select patterns are:
-abs [boolean]: selects the Absence specification pattern for testing when the boolean is true
-exis [boolean]: selects the Existence specification pattern for testing when the boolean is true
-univ [boolean]: selects the Universality specification pattern for testing when the boolean is true
-prec [boolean]: selects the Precedence specification pattern for testing when the boolean is true
-resp [boolean]: selects the Response specification pattern for testing when the boolean is true
-prec [boolean]: selects the Precedence specification pattern for testing when the boolean is true
-precc [boolean]: selects the Precedence Chain specification pattern for testing when the boolean is true
-respc [boolean]: selects the Response Chain specification pattern for testing when the boolean is true
-consc [boolean]: selects the Contrained Chain specification pattern for testing when the boolean is true
Not mentioning a specification patterns amounts to setting its Boolean flag to false.
Similarly, several other options are mandatory:
-n [integer>0] indicates the number of formulae to be monitored for each formula size,
-st [integer>0] indicates the size of the trace against which formulae will be monitored,
-dalpha [string_representation_of_a_distributed_alphabet] indicates the distributed alphabet to consider during the benchmark (See Section input formats).
Then one can choose the metrics and statistics that shall be displayed by using one of the following options:
-prt_full [bool] indicates that all statistics (number of messages, trace lengths and their ratio, but also the maximal and average delay) shall be displayed,
-prt_trace_mess [bool] indicates that trace and number of messages statistics") shall be displayed,
-prt_delay [bool] indicates that delay statistics shall be displayed.
---------------
A. Input formats |
---------------
We describe below some input formats that shall be used when submitting inputs for benchmark to DecentMon.
- Distributed alphabet:
They are represented by a quoted string. Distributed alphabets are delimited by curly braces. Inside a distributed alphabet the symbol '|' (resp. ',') is used to indicate component separation (reps. separate symbols inside a component).
For instance "{a1,a2|b1,b2|c1,c2}" denotes a 3-component architecture. On component 1 (reps. 2,3), the local alphabet contains symbols a1 and a2 (resp. b1 and b2, c1 and c2).
--------------------------------
B. LTL Specification Patterns |
--------------------------------
Those patterns come from the Specification Pattern Website (for LTL formulae): http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml.
Absence
P is false :
Globally [](!P)
Before R <>R -> (!P U R)
After Q [](Q -> [](!P))
Between Q and R []((Q & !R & <>R) -> (!P U R))
(*) After Q until R [](Q & !R -> (!P W R))
Existence
P becomes true :
Globally <>(P)
(*) Before R !R W (P & !R)
After Q [](!Q) | <>(Q & <>P))
(*) Between Q and R [](Q & !R -> (!R W (P & !R)))
(*) After Q until R [](Q & !R -> (!R U (P & !R)))
Bounded Existence
In these mappings we illustrate one instance of the bounded existence pattern, where the bound is at most 2 designated states. Other bounds can be specified by variations on this mapping.
transitions to P-states occur at most 2 times :
Globally (!P W (P W (!P W (P W []!P))))
Before R
<>R -> ((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P U R)))))))))
After Q <>Q -> (!Q U (Q & (!P W (P W (!P W (P W []!P))))))
Between Q and R
[]((Q & <>R) ->
((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P U R))))))))))
After Q until R
[](Q -> ((!P & !R) U (R | ((P & !R) U
(R | ((!P & !R) U (R | ((P & !R) U
(R | (!P W R) | []P)))))))))
Universality
P is true :
Globally [](P)
Before R <>R -> (P U R)
After Q [](Q -> [](P))
Between Q and R []((Q & !R & <>R) -> (P U R))
(*) After Q until R [](Q & !R -> (P W R))
Precedence
S precedes P:
(*) Globally !P W S
(*) Before R <>R -> (!P U (S | R))
(*) After Q []!Q | <>(Q & (!P W S))
(*) Between Q and R []((Q & !R & <>R) -> (!P U (S | R)))
(*) After Q until R [](Q & !R -> (!P W (S | R)))
Response
S responds to P :
Globally [](P -> <>S)
(*) Before R <>R -> (P -> (!R U (S & !R))) U R
After Q [](Q -> [](P -> <>S))
(*) Between Q and R []((Q & !R & <>R) -> (P -> (!R U (S & !R))) U R)
(*) After Q until R [](Q & !R -> ((P -> (!R U (S & !R))) W R)
Precedence Chain
This illustrates the 2 cause-1 effect precedence chain.
S, T precedes P:
Globally <>P -> (!P U (S & !P & o(!P U T)))
Before R <>R -> (!P U (R | (S & !P & o(!P U T))))
After Q ([]!Q) | (!Q U (Q & <>P -> (!P U (S & !P & o(!P U T))))
Between Q and R []((Q & <>R) -> (!P U (R | (S & !P & o(!P U T)))))
After Q until R [](Q -> (<>P -> (!P U (R | (S & !P & o(!P U T))))))
This illustrates the 1 cause-2 effect precedence chain.
P precedes (S, T):
Globally (<>(S & o<>T)) -> ((!S) U P))
Before R <>R -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P))
After Q ([]!Q) | ((!Q) U (Q & ((<>(S & o<>T)) -> ((!S) U P)))
Between Q and R []((Q & <>R) -> ((!(S & (!R) & o(!R U (T & !R)))) U (R | P)))
After Q until R [](Q -> (!(S & (!R) & o(!R U (T & !R))) U (R | P) | [](!(S & o<>T))))
Response Chain
This illustrates the 2 stimulus-1 response chain.
P responds to S,T:
Globally [] (S & o<> T -> o(<>(T & <> P)))
Before R <>R -> (S & o(!R U T) -> o(!R U (T & <> P))) U R
After Q [] (Q -> [] (S & o<> T -> o(!T U (T & <> P))))
Between Q and R [] ((Q & <>R) -> (S & o(!R U T) -> o(!R U (T & <> P))) U R)
After Q until R
[] (Q -> (S & o(!R U T) -> o(!R U (T & <> P))) U
(R | [] (S & o(!R U T) -> o(!R U (T & <> P)))))
This illustrates the 1 stimulus-2 response chain.
S,T responds to P:
Globally [] (P -> <>(S & o<>T))
Before R <>R -> (P -> (!R U (S & !R & o(!R U T)))) U R
After Q [] (Q -> [] (P -> (S & o<> T)))
Between Q and R [] ((Q & <>R) -> (P -> (!R U (S & !R & o(!R U T)))) U R)
After Q until R
[] (Q -> (P -> (!R U (S & !R & o(!R U T)))) U
(R | [] (P -> (S & o<> T))))
Constrained Chain Patterns
This is the 1-2 response chain constrained by a single proposition.
S,T without Z responds to P:
Globally [] (P -> <>(S & !Z & o(!Z U T)))
Before R <>R -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U R
After Q [] (Q -> [] (P -> (S & !Z & o(!Z U T))))
Between Q and R [] ((Q & <>R) -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U R)
After Q until R
[] (Q -> (P -> (!R U (S & !R & !Z & o((!R & !Z) U T)))) U
(R | [] (P -> (S & !Z & o(!Z U T)))))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment