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" IDENT

Observables 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