Fiacre Tutorial

Introduction

Fiacre stands for Format Intermédiaire pour les Architectures de Composants Répartis Embarqués (Intermediate Format for the Architectures of Embedded Distributed Components). It is a formal intermediate model to represent both the behavioural and timing aspects of systems, in particular embedded and distributed systems, for formal verification and simulation purposes.

Fiacre is built around two notions:

Processes describe the behaviour of sequential components. A process is defined by a set of control states, each associated with a piece of program built from deterministic constructs available in classical programming languages (assignments, if-then-else conditionals, while loops, and sequential compositions), nondeterministic constructs (nondeterministic choice and nondeterministic assignments), communication events on ports, and jumps to next state.
Components describe the composition of processes, possibly in a hierarchical manner. A component is defined as a parallel composition of components and/or processes communicating through ports and shared variables. The notion of component also allows to restrict the access mode and visibility of shared variables and ports, to associate timing constraints with communications, and to define priority between communication events.

Through this tutorial, you will learn how to use this language starting from the most basic system to a complete one.

A basic process

The most basic part of a system is a process. It describes a behaviour by the means of automata.

Let’s consider the following simple automaton:

The corresponding Fiacre process is introduced by the process keyword. It is where you declare the process name, as well as its parameters (we’ll see those later).

01    /* Let's define a nifty process! */
02    process ABC is

Fiacre comments are the same as in C and indentation is not significant.

Then the states keyword declares all the states of the process:

03      states a, b, c

We then declare a process transition from state a to state b:

04      from a
05        to b

The from keyword introduces a block of statements which perform actions (for instance, incrementing a counter) and eventually choose a next state using the jump statement to.

The first state to appear in the first transition of a process is always the initial state of this process.

You’ve got the idea:

06      from b
07        to c
08
09      from c
10        to a

The last statement of a Fiacre file indicates which process is the main entry of the specification:

11    ABC

Non-deterministic choice of states

Now, what if we want to introduce some non-determinism? Let’s consider the following automata which is a slight modification of the previous one:

The set of states is the same as before:

01    process ABC is
02
03      states a, b, c

The non-determism is introduced with the select keyword (don’t forget the closing end), the possible choices being seperated by []:

04      from a select
05         to b
06      [] to c
07      end

The select statement does what its name implies: it selects a statement to be executed, considering only statements for which all conditions hold. For now, there are no conditions and thus any statement can be selected. We’ll see such conditions later.

We see that a process transition can contain several different paths from a source state to a destination state, which at first can be quite confusing when considering the transitions of the corresponding automata. In fact, it’s simple: a path from a state to an other state in a process transition is a transition in the underlying automata. A such path is called a behavior transition in the Fiacre terminology.

The remaining transitions don’t change:

08      from b to c
09      from c to a
10
11    ABC

Variables and control-flow statements

From now on, we have seen the general shape of a process and how to describe its behavior. It’s now time to introduce variables and control-flow statements. Let’s consider this new automaton:

It loops while the i counter is less than 10 (the / character on an arc indicates the condition that must be verified to select the transtion followed by the action to be made.) Whether the value of the x counter if odd or even, a different transition is selected.

First, we define the type counter as a range from 0 to 10:

01    type counter is 0..10

Note that it’s not strictly necessary to define this type, but it’s more conveniant if we ever had several variables of counter type.

Then, as always, we declare the process name and its states:

02    process Loop is
03
04      states a, b, c, d

We then declare the local variables the process will use. The i counter is declared as a range of integers ranging from 0 to 10, while the x counter is declared as a natural integer with the nat keyword. Notice that the var keyword introduce all variables.

05      var i : counter := 0,
06          x : nat     := 0

You should consider using the most appropriate type for your data. For instance, if you need a counter that will never be greater than a given value, then using the appropriate interval is the right choice. While it won’t change your specification behavior, it will clearly state your intention and furthermore, the process verification could use considerably less memory. This is especially true for big specifications. Furthermore, the verification runtime will check that the range bounds are respected.

We then describe the transition from a to b with a sequence of three statements (be warry that ; separates two statements, it doesn’t indicate the end of a statement):

07      from a
08        i := i + 1;
09        on i < 10;
10        to b

The on keyword is a guard: the to b statement is only reached when i is less than 10. Because there is no other outgoing state we can reach from a, when i is greater than 10, the process will stay in a. In other words, on is a blocking statement. In this case, if i is less than 10, the state b is then reached:

11      from b
12        x := x + 1;
13        if x % 2 = 0 then
14          to c
15        else
16          to d
17        end

While in state b, whatever is the next state, we first increment x. Then, the next state is selected, the choice being based on the parity of x (% is the modulo operator).

The if statement needs some attention. Indeed, it’s possible to omit the else part
[Behind the scene, when omitting the else statement, the compiler insert a null statement, which, as the name implies, does nothing. Thus if cond then to a end is strictly equivalent to if cond then to a else null end.]
:

from b
  x := x + 1;
  if x % 2 = 0 then
    to c
  end

If we do so, the compiler will complain with the message "cannot compile: transition with no target state". The reason is that the if statement is a non blocking statement. Thus, if the condition is not verified, then the process goes through the conditonnal statement expecting an other to statement, which in this case does not exist, causing the compilation error.

So, a process must always be able to jump to another state, when not waiting on a blocking statement.

Now, let’s come back to our process. While in state c, the process should select a transition, the choice being made upon the parity of x. We could make this choice using an if statement again. But let’s take this opportunity to use instead the select statement to show how choices are guarded by conditions:

18      from c select
19         on x %2 = 0; to d
20      [] on x %2 = 1; to a
21      end

select is a blocking statement, meaning that if no condition holds, the process will wait in this statement until one condition is verified.

The state d follows the same principle as the state c, so let’s use a different way to express the transition selection. This time we use pattern matching with the case statement:

22      from d
23        case x %2 = 0 of
24          true  -> to a
25        | false -> to c
26        end

Contrary to the if statement, the case statement is blocking. This means that if we write this:

from d
  case x %2 = 0 of
    true  -> to a
  end

The process will be blocked in state d if x is odd (but the compiler will emit a warning saying that the pattern matching is not exhaustive).

As always, we finish with the declaration of the main process:

27    Loop

With this example, we’ve seen several ways to choose a transition to be fired, using if .. then .. else .. end, select .. end and case .. of .. end statements. Choosing between them is a matter of personal choice, but still, always keep in mind the blocking / non-blocking status of these statements.

Synchronization and communication

So far, we’ve seen how to write a single process. It’s now time to make several processes communicating together.

In this example, a process Master orders a process Slave to make him some good coffee or a nifty sandwich. In order to do so, we must be able to pass around these directives.

But first, let’s take this example as an opportunity to introduce a new type: unions. Fiacre unions are directly borrowed from the functional world, as such they can contain constructors with 0 or n parameters:

01    type Order is union
02        makeSandwich
03      | makeCoffee of 0..2
04      end

In our so realistic example, it’s obvious that a good sandwich is always made with tuna, so the order makeSandwich doesn’t need any parameter. But it’s also obious that we never know what kind of coffee we want, so the corresponding order makeCoffee takes a range as a parameter, to encode the coffee type.

Fiacre being targeted at real time systems, recursive data structures are forbidden.

Now, let’s focus on the slave. This poor being has the right to say only one thing: "ready master!", while eagarly waiting orders from its master:

05    process Slave [ready : none, order : in Order] is

The readiness status and the orders are communicated through the mean of labels. A process takes those labels as parameters between brackets (in fact, labels must appear as parameters of a process and cannot be declared locally to a process). We’ll see in a few moment how processes commmunicate through these labels, or, to be more precise synchronize together. But first, let’s take a look at those parameters.

Here, the first parameter ready is declared with type none. It is a predefined type that means that no value can be attached to this label. The second parameter order is declared of Order type, thus the type of value that can be transmitted with this label. Obviously, our slave cannot give orders to its master (or else, what is the point of being a slave?). Thus, the in keyword prefixes the type to indicate this harsh but necessary reality.

Then, we have all the possible states of the slave:

06      states startSlavery, waitOrder,
07             makingLatte, makingEspresso, makingCapuccino,
08             makingSandwich

We use a temporary variable to store the master’s order:

09      var tmp : Order

It start at its initial state:

10      from startSlavery

It’s now time to tell the master that the slave is ready:

11        ready;

And that’s all. Why is it so? Remember, we’ve talked about synchronizing processes, labels are not channels per se. The slave is not sending a message saying it’s ready, but synchronizing with its master, waiting for this latter one to be also synchronizing on this label (it’s thus a blocking statement). You can think of it as a communication when values are associated to labels, but still, it remains a synchronization.

When the synchronization is done, it’s time to jump into a state waiting for orders:

12        to waitOrder
13
14      from waitOrder

The slave is receiving an order when both slave and master are synchronizing on the order label. Though, the slave must take a decision using the value attached to the label. The ? symbol reads this value and puts it into the variable directly following it:

15        order?tmp;

Remember that it’s still a synchronization, so it’s a blocking statement.

After having read the order, we can use pattern-matching to choose the next state to reach:

16        case tmp of
17          makeCoffee(0) -> to makingLatte
18        | makeCoffee(1) -> to makingEspresso
19        | makeCoffee(2) -> to makingCapuccino
20        | makeSandwich -> to makingSandwich
21        end

It would also be possible to use a select statement, removing the need of a temporary variable:

from waitOrder select
   order?makeCoffee(0); to makingLatte
[] order?makeCoffee(1); to makingEspresso
[] order?makeCoffee(2); to makingCapuccino
[] order?makeSandwich; to makingSandwich
end

Finally, all working states will in the end return to the initial state:

22      from makingLatte
23        to startSlavery
24
25      from makingEspresso
26        to startSlavery
27
28      from makingCapuccino
29        to startSlavery
30
31      from makingSandwich
32        to startSlavery

The master waits for its minion to be ready in order to unleash upon him a flood of orders. So, like the slave, it synchronizes on the label ready, but only outputs orders, thus the value associated with the label order is declared as out:

33    process Master [ready : none, order : out Order] is
34
35      states start, ordering

First, the master synchronizes with the slave:

36      from start
37        ready;
38        to ordering

Then, it randomly outputs an order (remember that select is non-deterministic), writing into the value associated with the label being done with the ! symbol:

39      from ordering select
40         order!makeCoffee(0)
41      [] order!makeCoffee(1)
42      [] order!makeCoffee(2)
43      [] order!makeSandwich
44      end;

When the master has given its order, it can go back to its intial state:

45      to start

One could ask why we haven’t put all the interaction stuff into the same state. After all, whenever the synchronization with label ready is done, the master could directly output its orders. In fact, there is a rule in Fiacre which states that only one synchronisation can occur per transition.

We’ve seen two things: first, being the master is always easier. Second, the communication between processes is in fact a synchronisation with labels which are augmented with values. Now, we have to assemble those processes to "link" the labels.

This assembly is done with components:

46    component CruelWorld is

Processess cannot contain other processes while components can contain other components, possibly enabling recursive specifications.

Labels are declared in components with the port keyword:

47      port ready : none,
48           order : Order

Nothing tricky here, we use the same type as in our process signatures.

Then, we instanciate processes with these labels and launch them:

49      par
50         ready, order -> Slave  [ready, order]
51      || ready, order -> Master [ready, order]
52      end

So, what happens here? The par .. end block is the composition operator which describes what labels are to be synchronized. Directives of this composition are separated by ||. Let’s take a closer look a one of this directive: ready, order → Slave [ready, order]. The part after → is obviously the instantiation of the Slave process with the labels ready and order. The left part is simply the set of labels to be synchronized for this particular instance, which, in this case, is the set of all labels.

To avoid cumbersome compositions, we can factorize the common labels:

par ready, order in
   Slave  [ready, order]
|| Master [ready, order]
end

Which is much better. But an handy shortcut provides this in an even better way:

par * in
   Slave  [ready, order]
|| Master [ready, order]
end

Finally, the entry of the specification is the component itself:

53    CruelWorld

Note that the label ready is not strictly necessary, synchronizing on order is sufficiant as the master has to wait that the slave is reading the value associated with order. It was merely to illustrate the type of values transmitted with labels as well as the rule of one synchronization per transition.

Shared variables

It’s possible to pass informations around with an other mechanism than labels: shared variables. To illustrate the use of these variables, let’s refine our previous specification of master and slave. This time, we’ll add some slaves to do more work at the same time. And, contrary to the previous exxample, we won’t use a machanism to express that all slaves are ready.

Fiacre provides the queue type which we will use in this example to pass a set of orders from the master to the slaves. The queue being not empty is sufficient to indicate that there orders to perform and thus removing the need of readiness status.

We still have the same kind of orders:

01    type Order is union
02        makeSandwich
03      | makeCoffee of 0..2
04      end

We declare the type based on a queue that will contain orders:

05    const MAX_ORDERS : nat is 3
06    type Orders is queue MAX_ORDERS of Order

Queues are always bounded.

Like in the previous example, the process Slave is parametrized, but this time with a shared variable (notice that variables are between parenthesis this time):

07    process Slave (&orders : read write Orders) is

Notice the & before the parameter name: it means that it’s passed as a reference. Omitting & would end in copying the value. The read write attributes are self-descriptive.

A process can be parametrized by labels and variables, the labels appearing before the variables: process P [labels] (variables).

First, we declare all the states that a slave can reach:

08      states waitOrder,
09             makingLatte, makingEspresso, makingCapuccino,
10             makingSandwich

We need a temporary variable to store the order on the top of the orders queue coming from the master:

11      var order : Order

A Fiacre queue has several functions to interact with:

12      from waitOrder
13        on not (empty(orders));
14        order  := first orders;
15        orders := dequeue orders;

The first statement on blocks this transition while there are no orders to read. Then, the first function returns the oldest element in the queue, but doesn’t remove it. This is what the dequeue function is intended for. Note that dequeue doesn’t modify the queue in-place. Rather, it returns a modified copy.

We shall take this transition as an opportunity to enforce an important idea: atomicity. Transitions are performed totally or not started at all. If some condition along some execution path is not fullfilled, then that path does not yield a behavior (we say the path is blocking). Furthermore, only one transition at a time can occur. This is why we can safely interact with the queue as we are absolutly certain that no other process will interact with it.

Then, as in the previous example, the slave jumps to a state according to the order:

16        case order of
17          makeCoffee(0) -> to makingLatte
18        | makeCoffee(1) -> to makingEspresso
19        | makeCoffee(2) -> to makingCapuccino
20        | makeSandwich -> to makingSandwich
21        end
22
23      from makingLatte
24        to waitOrder
25
26      from makingEspresso
27        to waitOrder
28
29      from makingCapuccino
30        to waitOrder
31
32      from makingSandwich
33        to waitOrder

Like the slaves, the master takes a queue order, though it just needs to write into it:

34    process Master (&orders : read write Orders) is

Only one state is needed as the master will only output orders:

35      states ordering
36
37      from ordering
38        on not (full(orders));
39        select
40           orders := enqueue(orders, makeCoffee(0))
41        [] orders := enqueue(orders, makeCoffee(1))
42        [] orders := enqueue(orders, makeCoffee(2))
43        [] orders := enqueue(orders, makeSandwich)
44        end;
45        to ordering

The first statement of the transition blocks while the queue is full. When there is some room, it creates randomly a new order and puts at the beginning of the queue with enqueue. Like dequeue, enqueue doesn’t modify the queue, but outputs a new one.

Finally, we assemble all processes together:

46    component CruelWorld is

Components can declare local variables to be passed to sub-processes (or sub-components). A queue is initialized with an expression of the form {|…|}. Let’s add some initial orders:

47      var orders : Orders := {|makeSandwich, makeCoffee(1)|}

Components' local variables must always be initialized.

Even if we don’t use labels, the par block is still used to instanciate and launch processes:

48      par
49         Master(&orders)
50      || Slave(&orders)
51      || Slave(&orders)
52      end

Also, notice that & is used on both sides of the callee and the caller to express the shared state of a variable.

And as always, the declaration of the entry of the specification:

53    CruelWorld

Conclusion

Through this tutorial, you’ve seen how to write a Fiacre specification. Basically, there are two important rules to remind of:

Transitions are atomic: a transition is performed totally or not at all. Furthermore, only one transition can be performed at a time.
Only one synchronization can be performed per transition.

A complete reference is available on http://www.laas.fr/fiacre.