GPSL syntax
Generic Property Specification Language (GPSL) is the language used by OBP2 for specifying the properties that should be verified during the analysis (aka LTL for Plug).
In GPSL each property is associated with a named variable. All these variables form the property set Any subset of the property set can be verified during an analysis run.
Assertions: Syntax & Semantics
There are two Boolean constants predefined in the language: true and false
Atomic proposition in GPSL are strings of characters enclosed between pairs of | (ie. | string of characters |). Each atomic proposition can be prefixed with two identifiers specifying the atomic proposition language and the ‘verification’ module on which it should be interpreted.
Boolean Operators
Two expressions f and g can be combined using the following Boolean operators
| Operation | syntax0 | syntax1 | syntax2 | syntax3 | syntax4 |
|---|---|---|---|---|---|
| negation | not f | !f | ~f | ||
| disjunction | f or g | f | g | f \/ g | f + g | |
| conjunction | f and g | f & g | f && g | f /\ g | f * g |
| exclusion | f xor g | f ^ g | |||
| implication | f implies g | f -> g | f => g | ||
| equivalence | f iff g | f <-> g | f <=> g |
Let Expressions
To simplify the expression of large formula GPSL uses Let expression forms to introduce variables.
let
v1 = expr
v2 = expr
...
vn = expr
in
v1 op v2
Temporal Logic: Syntax & Semantics
The support for LTL is enabled using LTL3Buchi conversion [1].
Temporal Logic Operators
Two expressions f and g can be combined using the following Boolean operators
| operation | syntax0 | syntax1 | syntax2 |
|---|---|---|---|
| Next | X f | next f | () f |
| Eventually | F f | eventually f | <> f |
| Always | G f | globally f | [] f |
| Strong Until | f U g | f until g | |
| Weak Until | f W g | ||
| Weak Release | f R g | f release g | f V g |
| Strong Release | f M g |
Some examples
aliceCS = |{Alice}1@CS|
bobCS = |{Bob}1@CS|
exclusionI = []!(|{Alice}1@I| && |{Bob}1@I|)
exclusion = []!(aliceCS && bobCS)
eventuallyOneInCS = []<>(aliceCS || bobCS)
fairness =
let
aliceFlagUP=|{sys}1:flags[0] = true|,
bobFlagUP=|{sys}1:flags[1] = true|
in
([] ( (aliceFlagUP -> (<> aliceCS) )
&& (bobFlagUP -> (<> bobCS))))
idling = let
aliceFlagUP=|{sys}1:flags[0]=true|,
bobFlagUP=|{sys}1:flags[1]=true|
in
([] (!aliceFlagUP -> (![] aliceCS))
&& (!bobFlagUP -> (![] bobCS)) )
infoften = [] <> bobCS
all = (exclusion & eventuallyOneInCS & fairness & idling)
References
[1] Babiak, Tomáš, et al. “LTL to Büchi automata translation: Fast and more deterministic.” International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2012.