The IF-language was proposed in order to model asynchronous communicating real-time systems. For full details of IF see here. It is also the common model description language of the ADVANCE project.

We show the main concepts of IF by showing how Dekker's mutex algorithm can be specified in IF.

In [RAY86] Dekker's mutex algorithm is described as follows:

     var flag: array[0..1] of boolean;
     var turn: 0..1;

flag is initialized to false, and turn has the value 0 or 1.

The protocol for process i then becomes:

     flag[i] := true;
     while flag[j] do if turn = j then
                         begin
                              flag[i] := false;
                              while turn = j do nothing enddo;
                              flag[i] := true;
                         end;
                       endif;
                    enddo;
     [critical section];
     turn := j;
     flag[i] := false;

The corresponding IF specification looks like:

system dekker;

type int = range 0..1;

var flag0 int;
var flag1 int;
var turn int;

process p0(1);


state a #start;

task flag0 := 1;
nextstate b;

endstate;
state b;

provided flag1 = 1 and turn = 1;

task flag0 := 0;
nextstate c;

provided flag1 = 0;

nextstate incs0;

endstate;
state c;

provided turn = 0;

task flag0 := 1;
nextstate b;

endstate;
state incs0;

task turn := 1;
nextstate d;

endstate;
state d;

task flag0 := 0;
nextstate a;

endstate;

endprocess;

process p1(1);


state a #start;

task flag1 := 1;
nextstate b;

endstate;
state b;

provided flag0 = 1 and turn = 0;

task flag1 := 0;
nextstate c;

provided flag0 = 0;

nextstate incs1;

endstate;
state c;

provided turn = 1;

task flag1 := 1;
nextstate b;

endstate;
state incs1;

task turn := 0;
nextstate d;

endstate;
state d;

task flag1 := 0;
nextstate a;

endstate;

endprocess;

endsystem;

Now one can check the mutex property like this:

check if:pep-reach dekker.if mutex.if_form

The following output should be printed on your screen:

Time needed: 0.350000 seconds
Result: NO.

We have implemented an interface between the common description language (IF) and the Kit. It includes a a compiler from IF into safe Petri Nets (the basic model of the Kit), a formula converter which translates properties of the original model into Petri net properties, and a trace interpreter which translates error traces of the Petri net back into traces of the original model. The fragment covered by the compiler excludes the real-time features of the language and is limited to finite data types (since these cannot be modeled in the target language), but includes important features like dynamic process creation or different signal delivery disciplines.

More precisely, the list of supported features is as follows:

• Systems consist of multiple processes running in parallel; multiple instances of a process can exist simultaneously, but the maximum number of concurrently active instances has to be fixed a priori.
• Processes can communicate by exchanging signals or through shared variables. Signals (which may take arguments) can pass either through signalroutes or through direct communication between processes. Incoming signals are stored in a message queue. A limitation is that the capacity of the message queue has to be fixed a priori.
• Signalroute can have different delivery disciplines in the common language most of which are supported by the compiler: FIFO and multiset queueing, reliable and lossy transmission, peer-to-peer, unicast, and multicast delivery. Moreover, the common language provides for urgent (immediate) and delayed delivery. In the case of delayed delivery, the language allows to place temporal constraints on the amount of delay and the transmission rate. These temporal restrictions are not supported by the compiler, but distinction is made between immediate and delayed delivery where signals are stored in a buffer (of fixed size).
• The following data types are supported by the compiler:
  • finite integer fragments
  • process/signalroute ids
  • booleans
  • enum and range types
  The following types are not supported
  • floats, clocks and unbounded integer types
  • arrays and records (though these could be added if necessary)
  • strings and abstract types
• Procedures (which are used to import C code into the system) are not supported.
• Of the guards that control entry into a state transition, we support the input and the provided guards. The temporal guards tpc, deadline, or when are not supported. Save sets are not currently supported, but can be considered for implementation if needed.
• Of the actions available inside state transitions, we support manipulation of variables (task), sending of signals (output), and the dynamic creation of processes (complete with the passing of arguments) and signalroutes, as well as process/signalroute destruction (kill). Actions to do with clocks (set/reset) are not supported.

Atomic propositions in formulae

We give the atomic propositions in Backus-Naur notation.

AtomicProposition:

ProcessInstance.signals ArithOp Value

| SignalrouteInstance.signals ArithOp Value

| ProcessIdent.instances ArithOp Value

| SignalrouteIdent.instances ArithOp Value

| ProcessInstance.VariableIdent ArithOp Value

| ProcessInstance.state = StateName

| ProcessInstance.queue[Value].signal = SignalName

| SignalrouteInstance.queue[Value].signal = SignalName

| SignalrouteInstance.queue[Value].receiver = ProcessValue

| ProcessInstance.overflow

| SignalrouteInstance.overflow

| ProcessInstance.active

ProcessInstance:

ProcessIdent

| ProcessIdent[z]

(z in N)

| ProcessIdent[VariableIdent]

SignalrouteInstance:

SignalrouteIdent

| SignalrouteIdent[z]

(z in N)

| SignalrouteIdent[VariableIdent]

ArithOp:

= | # | < | <= | > | >=