Testing the Correctness of a Realtime Observer

We study an example involving the notions of probes and observers in Fiacre. The problem is to check the validity of a high-level specification pattern (see this page for information on properties in Fiacre).

We assume that you have already installed Tina and the Fiacre compiler, named frac. Tina can be used to generate the state graph of a model (files with the extension .aut, .adr and .ktz below). The tina distribution also provides two model-checkers: selt for model-checking linear (LTL) properties and muse for checking branching (CTL or modal mu-calculus) properties.

The input models of Tina can be Time Petri Nets (TPN), either in textual (.net) or graphical (.ndr) format, or an extended notion of TPN with priorities and variables, called a Time Transition System (TTS). TTS models can be generated by compiling Fiacre specifications (files with the extension .fcr below). We provide a Makefile that can be used to compile the examples in this page. (Actually we provide two different files, one for UNIX-like OS and the other for Windows.) You must edit the Makefile to specify the path to your local installation of Fiacre (variable FRACLIB) and the type of operating system (variable HOSTTYPE).

Simple Example of Observers and Properties in Fiacre: the Computer Mouse Example

Our first model is a simple version of the specification of a computer mouse with a double click in Fiacre. We provide two versions of the model: first a Fiacre model with two property declarations (file mouseProperty.fcr); then the same model with a different property expressed using an observer (file mouseObserver.fcr). This is the example used for describing the Fiacre language in the companion paper [TTCS15].

Files with the extension .fcr can be compiled into a TTS using the frac compiler. Using the Makefile provided with the source files we can generate the TTS files using the following command. (We use the symbol $> for the shell prompt.) $> make mouseObserver.tts
frac -obs .\mouseObserver.fcr .\mouseObserver.tts
gcc -m32 -DMINGW -O2 -o .\mouseObserver.tts\mouseObserver.dll -shared -I C:\Users\...\frac-2.2.4\lib -I C:\Users\...\frac-2.2.4\lib\avl .\mouseObserver.tts\mouseObserver.c

We can generate the state space of the TTS model using the tina tool. The following command will generate a state graph in compressed form (extension .ktz); it is possible to list the data in this file using the ktzio tool.

$> tina .\mouseProperty.tts mousep.ktz # net process_____presentAfter____2__1_________presentAfter________1____1__Computer____1____User____1____Push____1, 19 places, 19 transitions# # bounded, not live, possibly reversible # # abstraction count props psets dead live # # states 1836 19 ? 0 40 # # transitions 2407 19 ? 1 11 #  $> ktzio .\mousep.ktz

Checking the Properties in File mouseProperty.fcr

The model in mouseProperty.fcr has two property declarations:

property foo is present (Main/3/state two) after (Main/2/state quick) within [1,2]
property bar is present (Main/3/state two) after (Main/2/state slow) within [0,100]

These properties are related to events declared in the main component of the specification (called Main), see the code excerpt below. Hence, for example, the declaration Main/2 targets the events of the second process instance in the parallel composition in Main (that is an instance of the process User)

component Main is port click, single, double : none in [0,0]
par * in
Mouse [click, single, double]
|| User [click]
|| Computer [single, double]
end

Main

The computer mouse model is composed with two other processes, modeling a User and a Computer, which describes the behavior of the environment. Property foo states that after the User presses quickly in the mouse button (it is in state quick) then we must observe the process Computer in state two between 1 and 2 units of time.

Properties are automatically translated into LTL formulas (see the file mouseProperty.tts/mouseProperty.ltl in the generated TTS) that can be checked as follows. We use the command line options -b -q to simply print the truth value of the two asserts directives. You can find more information on the manual pages of selt

$> selt -b -q .\mousep.ktz .\mouseProperty.tts\mouseProperty.ltl TRUE FALSE Checking the Properties in File mouseObserver.fcr The model in mouseObserver.fcr has a single property. This is a LTL formula stating that the observer NeverTwice will never reach the state error. The command-line option -obs of frac is necessary when compiling a model that uses observers. property safe is ltl [] not (Obs/1/state error)  In this model, the observer component Obs is not part of the main component but it can observe when Computer enters its state named two using the probe p (the probe is declared as enter (Main/3/state two)). Hence the property safe is true only if Computer cannot enter twice in the state two. This can be checked using the following command. $> tina mouseObserver.tts mouseo.ktz
...

$> tina -F1 universalpresent.tts univ.aut WARNING: dense traces not preserved, some priorities # net process_Present__1_Universal__1, 6 places, 7 transitions # # bounded, not live, not reversible # # abstraction count props psets dead live # # states 26 0 ? 0 6 # # transitions 43 7 ? 0 3 #  The labels of the state graph in univ.aut are generated from the names of the processes together with an identifier, e.g. t0, that identifies uniquely a transition in the process. The AUT format (also called Aldebaran format) is a simple textual format for representing labelled transition systems that can be used with several model-checking toolboxes. An AUT file can be opened in the nd tool; this is an editor and TPN simulator that is part of the Tina distribution (see for example here). It is possible to generate a graphical version of the graph using an automatic layout; just go to the menu toolbar in nd, under Edit > draw then choose a layout algorithm. In the remainder of this work, we use a version of the AUT file where labels are renamed to follow the convention in our paper. This is the file verif.aut below. We also provide a graphical version of the file. • verif.aut • verif.adr (same system, graphical file) • verif.ktz (same system, compressed format, can be obtained with the command ktzio .\verif.aut .\verif.ktz) The next step is to study the soundness and the completeness of our observer with respect to the semantics of the pattern. We remark in the paper [TTCS15 that, in the discrete time case, it is possible to define the semantics of the pattern using a regular (path) expression. Namely, if Tick stands for the expression t . (-t)* then we have: Pres = (-b)* \/ ((-b)* · b · (- t)* · Tick · Tick · Tick · Tick · a · T*) Checking the Soundness of the Observer using LTL It is a folklore result that regular expressions can be interpreted as temporal logic formulas. Next, we use the connection between regular expressions and LTL to check the soundness of the Present observer. We study the limitation of this approach and show that the use of a branching logic is more interesting. We can use LTL formulas to interpret regular expressions. For instance the expression (-b)* (never b) can be interpreted by the formula [] -b (always not b). More generally, the (finite) traces matching the expression Pres can be encoded with the following formulas and checked using selt. $> more .\present.ltl
infix L o R  = L /\ ()R;
infix L * R  = L U R;
op TICK R    = t o ((- t) * R);

op Phi1 = [] - b;
op Phi2 = (-b) * (b o ((-t) * (TICK (TICK (TICK (TICK (a o T)))))));

(Phi1 \/ Phi2) => ([] - error);

([] - error) => (Phi1 \/ Phi2);

...
EQUIV : states
TRUE


Files Available on this Use Case

Everything in a single archive file.

References

[TTCS15] Automating the Verification of Realtime Observers using Probes and the Modal mu-calculus. Silvano Dal Zilio and Bernard Berthomieu, submitted. 2015