frac properties
As of version 1.7.0, frac supports declarations of properties and assert directives. Properties are defined from observables (or probes); the language of properties include LTL properties, Dwyer et al. patterns, and timed extensions of the latter (work in progress).
Observables, or probes
An observable describes a state property or a set of transitions of a fiacre specification. They obey the following syntax:// observables o ::= path item | "enter" o | "leave" o | "not" o | o "and" o | o "or" o | o "=>" o | "(" o ")" path ::= IDENT "/" (NAT "/")* item ::= "state" IDENT | "value" exp | "tag" IDENT | "event" IDENTObservables play the role of atomic proposition in the properties. Their meanings is as follows:
-
path/state s:
- is true if the process instance identified by path is in state s
path/value p:
- is true if predicate p is true in the process instance identified by path
path/tag t:
- is the set of transitions of the process instance
identified by path bearing tag s (tags may by inserted
in process sources by the user, as statements of form
"#ident")
path/event p:
- is the set of transitions interacting on port p declared
in the component identified by path;
Properties
A fiacre description may include declarations of properties and "assert" directives. The language of declarations is extended by:
"property" IDENT "is" p "assert" IDENT {-true STRING} {-false STRING}
When compiling a fiacre description, frac generates, in
addition to the usual .c and .net files, a .ltl file (also in
directory .tts) containing a list of declarations of selt properties
(each corresponding with some fiacre property in the fiacre
description) and a list of verification requests (one for each
"assert" directive in the fiacre description).
The set of properties includes "general" properties, "pattern"
properties, and property combinators. Properties obey the following
grammar.
// time intervals (NAT are nonnegative integers) i ::= ("[" | "]") NAT "," (NAT ("]" | "[") | "...[") // durations d ::= NAT // ltl properties (ltl on observables) l ::= o // observable | "[]" l // always | "<>" l // eventually | "()" l // next | "not" l | l "and" l | l "or" l | l "=>" l | l "until" l // until | l "release" l // release | "(" l ")" // properties p ::= // ltl properties "ltl" l // general | "deadlockfree" | "infinitelyoften" o | "mortal" o // presence patterns | "present" o | "present" o "after" o | "present" o "before" o | "present" o "between" o "and" o | "present" o "after" o "until" o | "present" o "within" i | "present" o "lasting" d | "present" o "after" o "within" i | "present" o "before" o "within" i // absence patterns | "absent" o | "absent" o "after" o | "absent" o "before" o | "absent" o "between" o "and" o | "absent" o "after" o "until" o | "absent" o "within" i | "absent" o "after" o "within" i | "absent" o "before" o "for" d // response patterns | o "leadsto" o | o "leadsto" o "before" o | o "leadsto" o "after" o | o "leadsto" o "between" o "and" o | o "leadsto" o "after" o "until" o | o "leadsto" o "within" i | o "leadsto" o "before" o "within" i | o "leadsto" o "after" o "within" i // universality patterns | "always" o | "always" o "after" o | "always" o "before" | "always" o "between" o "and" o | "always" o "after" o "until" o // precedence patterns | o "precedes" o | o "precedes" o "before" o | o "precedes" o "after" o | o "precedes" o "between" o "and" o | o "precedes" o "after" o "until" o // compositions | p "and" q | p "or" q | p "=>" q | "not" p // parentheses | "(" p ")"
The semantics of untimed patterns is exactly that of Dwyer et al. patterns patterns on http://patterns.projects.cis.ksu.edu (see also [DAC99]).
Usage:
By default, frac parses properties and assert directives.
frac -strip removes from a description all tag annotations, property declarations and assert directives, and disables generation of the .ltl file.
References
[DAC99] Matthew B. Dwyer, George S. Avrunin, James C. Corbett Patterns in property specifications for finite-state verification ICSE '99 Proceedings of the 21st international conference on Software engineering ACM New York, NY, USA, 1999 ISBN:1-58113-074-0
[Patterns] http://patterns.projects.cis.ksu.edu