The Syntax and Semantics of FIACRE

Bernard Berthomieu∗, Jean-Paul Bodeveix^{+}, Mamoun Filali^{+}, Hubert Garavel†, Frédéric Lang†, Florent Peres∗, Rodrigo Saad∗, Jan Stoecker†, François Vernadat∗

Version 2.0

March 17, 2009

∗ LAAS-CNRS Université de Toulouse

7, avenue du Colonel Roche, 31077 Toulouse Cedex, France

E-mail: FirstName.LastName@laas.fr

+ IRIT Université Paul Sabatier

118 Route de Narbonne, 31062 Toulouse Cedex 9, France

E-mail: FirstName.LastName@irit.fr

† INRIA

Centre de Recherche de Grenoble Rhône-Alpes / équipe-projet VASY

655, avenue de l’Europe, 38 334 Saint Ismier Cedex, France

E-mail: FirstName.LastName@inria.fr

1 Introduction

This document presents the syntax and formal semantics of the Fiacre language, version 2.0. Fiacre is an acronym for Format Intermédiaire pour les Architectures de Composants Répartis Embarqués (Intermediate Format for the Architectures of Embedded Distributed Components). Fiacre 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 embeds the following 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.

Fiacre was designed in the framework of projects dealing with model-driven engineering and gathering numerous partners, from both industry and academics. Therefore, Fiacre is designed both as the target language of model transformation engines from various models such as Sdl or Uml, and as the source language of compilers into the targeted verification toolboxes, namely Cadp [8] and Tina [3] in the first step. In this document, we propose a textual syntax for Fiacre, the definition of a metamodel being a different task, out of the scope of this deliverable.

Fiacre was primarily inspired from two works, namely V-Cotre [4] and Ntif [7], as well as decades of research on concurrency theory and real-time systems theory. Its design started after a study of existing models for the representation of concurrent asynchronous (possibly timed) processes [5]. Its timing primitives are borrowed from Time Petri nets [11, 2]. The integration of time constraints and priorities into the language was in part inspired by the BIP framework [1]. Concerning compositions, Fiacre incorporates a parallel composition operator [9] and a notion of gate typing [6] which were previously adopted in E-Lotos [10] and Lotos-NT [12, 13].

This document is organized as follows: Section 2 presents the concrete syntax of Fiacre processes, components, and programs. Section 3 presents the static semantics of Fiacre, namely the well-formedness and well-typing constraints. Finally, Section 4 presents the formal dynamic semantics of a Fiacre program, in terms of a timed state/transition graph.

2 Concrete syntax

2.1 Notations

We describe the grammar of the Fiacre language using a variant of EBNF (Extended Bachus Naur Form). The EBNF describes a set of production rules of the form “symb ::= expr”, meaning that the nonterminal symbol symb represents anything that can be generated by the EBNF expression expr. An expression expr may be one of the following:

• a keyword, written in bold font (e.g., type, record, etc.)

• a terminal symbol, written between simple quotes (e.g., ’:’, ’(’, etc.)

• a nonterminal symbol, written in teletype font (e.g., type, type decl, etc.)

• an optional expression, written “[ expr_{0} ]”

• a choice between two expressions, written “expr_{1} | expr_{2}”

• the concatenation of two expressions, written “expr_{1} expr_{2}”

• the iterative concatenation of zero (resp. one) or more expressions, written “expr^{∗}” (resp. “expr^{+}”)

• the iterative concatenation of zero (resp. one) or more expressions, each two successive occurrences being separated by a given symbol s, written “exprs^{∗}” (resp. “exprs^{+}”)

The star and plus symbols have precedence over concatenation. Parentheses may be used to group a sequence of expressions when iterative concatenation concerns the whole sequence.

2.2 Lexical elements

IDENT ::= any sequence of letters, digits, or '_', beginning by a letter
NATURAL ::= any nonempty sequence of digits
INTEGER ::= ['+'|'-'] NATURAL
DECIMAL ::= NATURAL ['.' [NATURAL]] | '.' NATURAL

No upper bound is specified for the length of identifiers or numeric constants. The code generation pass will check that numeric constants can indeed be interpreted.

Comments:

A comment is any sequence of characters between the comment brackets ’/*’ and ’*/’ in which comment brackets are properly nested.

Reserved words and characters:

Keywords may not be used as identifiers, these are:

and any append array bool case channel component const dequeue do
else elsif empty end enqueue false first foreach from full if in init int is
nat none not null of or out par port priority process queue read record
select states then to true type union var where while write

The following characters and symbolic words are reserved:

         [] [  ]  (  ) { } {|  |} :  ...  ..  .  =  <>  <  >  <=  >=
         +  -  * /  %  $  & |  || :=  ;  , ?  !  ->  #  /*  */

2.3 Types, type declarations

type id ::= IDENT
constr ::= IDENT
field ::= IDENT
type ::=

bool | nat | int

    | type id
    | exp '..' exp
    | union (constr,^{+} [of type])|^{+} end [union]
    | record (field,^{+} ':' type),^{+} end [record]
    | array exp of type
    | queue exp of type

The exp’s in types are functional expressions. They may make use of declared constants (see Section 2.4). They should evaluate to nonnegative integers (in array and queue types, in which they specify sizes) or to integers (in interval types, in which they specify the interval bounds).

type decl ::= type type id is type

2.4 Expressions, constant declarations

unop ::= '-' | '+' | '$' | not | full | empty | dequeue | first

binop ::= enqueue | append

infixop ::=

or | and

| '=' | '<>' |
| '<' | '>' | '<=' | '>='
| '+' | '-'
| '*' | '/' | '%'

Infix operators are listed in order of increasing precedence, those in same line have same precedence. All are left associative.

var ::= IDENT
literal ::= INTEGER | true | false
atomexp ::= literal | var | constr | '(' exp ')'
accessexp ::= atomexp | accessexp '[' exp ']' | accessexp '.' field
exp ::=
  accesexp
| constr [atomexp]
| unop atomexp
| binop '(' exp ',' exp ')'
| exp infixop exp
| exp '?' exp ':' exp

| '[' exp,^{+} ']'

| '{' (field '=' exp),^{+} '}'

| '{|' exp,^{∗} '|}'

const decl ::= const var ':' type is exp

2.5 Ports, channels, channel declarations

port := IDENT
channel_id ::= IDENT
channel ::= none | type#^{+} | channel_id
channel_decl ::= channel channel_id is channel

A port is a process communication point. Ports can be used to exchange data. A port type, or channel, determines the type of data that can be exchanged on the port. Channels specified by a series of types separated by '#' are associated with ports transfering several values simultaneously. A port having channel none may be used as a synchronization port (without any value transfered).

2.6 Processes

state ::= IDENT
name ::= IDENT
left ::= '[' DECIMAL | ']' DECIMAL
right ::= DECIMAL ']' | DECIMAL '[' | '...' '['
time_interval ::= left ',' right
port dec ::= port,^{+} ':' [in] [out] channel

Ports may have the optional in and/or out attributes, specifying that values may only be received and/or sent through that port. By default, ports have both the in and out attributes. The attributes and channel of a port may be omitted when shared with the following port in the declaration.

arg dec ::= ([&] var),^{+} ':' [read] [write] type

The parameters preceded by symbol & are passed by reference, the others are passed by value. Parameters passed by reference may have the read and/or the write attribute, specifying the operations that can be done on the variable, by default they have both attributes. The attributes and type of a parameter may be omitted when shared with the following parameter in the declaration.

var dec ::= var,^{+} ':' type [':=' exp]

Initial values are optional, they may also be specified by an initialisation statement (see below). The type and initial value of a variable may be omitted when shared with the following variable in the declaration.

transition ::= from state statement
atompatt ::= any | literal | var | constr | '(' pattern ')'
accesspatt ::= atompatt | accesspatt '[' exp ']' | accesspatt '.' field
pattern ::= accesspatt | constr [atompatt]
statement ::=

null

    | pattern,^{+} ':=' exp,^{+}
    | pattern,^{+} ':=' any [where exp]
    | while exp do statement end [while]

| foreach var do statement end [foreach]

| if exp then statement (elsif exp then statement)* [else statement] end [if]

| select statement[]^{+} end [select]

| case exp of (pattern '->' statement)|^{+} end [case]
| to state
| statement ';' statement
| port
| port '?' pattern,^{+} [where exp]

| port '!' exp,^{+}

Additional well-formedness constraints are given in Section 3. The last three statement are referred to as “communication” statements.

process decl ::=

process name

   ['[' port_dec,^{+} ']']

   ['(' arg_dec,^{+} ')']

is states state,^{+}

   [var var_dec,^{+}]
   [init statement]
   transition^{+}

Name of the process, port parameters, functional parameters or references, states and initial state, local variables, followed by an optional initialization statement and a series of transitions. The initialization statement may not perform communications nor read or write variables passed by reference.

2.7 Components

arg ::= exp | '&' var
instance ::= name ['[' port,^{+} ']']  ['(' arg,^{+} ')']

Instance of a process or component. Arguments passed by reference are prefixed by symbol &.

portset ::= '*' | port,^{+}
compblock ::= instance | composition
composition ::=
| par [portset in] ([portset '->'] compblock)||^{+} end [par]
component decl ::=

component name

   ['[' port_dec,^{+} ']']

   ['(' arg_dec,^{+} ')']

is [var var_dec,^{+}]

  [port (port_dec [in time_interval]),^{+}]
  [priority (port|^{+} '>' port|^{+}),^{+}]
  [init statement]
  composition

Name of the component, port parameters, functional parameters or references, local variables or references, local ports with delay constraints, priority constraints, followed by an optional initialization statement and a composition. The initialization statement may not include communications or to statements, nor read or write variables passed by reference. In priority declarations, a_{1}|...|a_{n} > b_{1}|...|b_{m} is a shorthand for (∀i ∈ {1, …, n})(∀j ∈ {1, …, m})(a_{i}> b_{j}).

2.8 Programs

declaration ::=
 type decl
| channel decl
| const decl
| process decl
| component decl
program ::=
declaration^{+}
name

The body of a program is specified as the name of a process or component. If that process or component admits parameters, then these parameters are parameters of the program.

3 Static semantics

3.1 Well-formed programs

3.1.1 Constraints A program is well-formed if its constituents obey the following static semantic constraints.

1. Process and component identifiers should all be distinct;

2. Type and channel identifiers should all be distinct;

3. In any record type all labels declared must be distinct;

4. In any union type all constructors declared must be distinct;

5. In declarations of ports, formal parameters, or local variables, all identifiers must be distinct;

6. In a state declaration, all states must be distinct;

7. There is a single syntactical class for shared variables, formal parameters of processes or components, local variables, and union constructors. As a consequence, the sets of shared variable identifiers, formal parameter identifiers, local variable identifiers and constructors identifiers (declared globally or in the header of some process or component) should be pairwise disjoint;

8. No keyword (e.g. if, from, etc) may be used as the name of a component, process, variable, constructor, type, channel or port;

9. In any interval type x..y, one must have x ≤ y;

10. In a process, there may be at most one transition from each state declared;

11. In timed local port declarations, time intervals may not be empty (e.g. intervals like [7, 3[ or ]1, 1] are rejected);

12. In a priority declaration, the transitive closure of priority relation defined must be a strict partial order;

13. In an assignment statement, the access expressions in the left-hand side must be pairwise independent. A sufficient condition for that constraint is explained in Section 3.1.2;

14. In any transition, at most one communication statement may be found along any execution path and, along any path including a communication statement, no shared variable may be read or written. This constraint, referred to as the single-communication constraint is integrated with the well-typing condition for statements, see Section 3.2.5;

15. In any process, local variables or their constituents should be initialized before their first use, a sufficient static condition ensuring that property is discussed in Section 3.1.3; 3.1.2 Well-formedness of assignment statements:

Assuming constants are replaced by their values (their values must be statically computable), left hand sides of assignment statements have the shape of series of access expressions possibly surrounded by a series of constructors. Each access expression is a sequence a_{0} a_{1} … a_{n} where a_{0} is some variable and each a_{i} (i > 0) is either a field access (shape .f) or an array component access (shape [exp]).

Two patterns are independent if, omitting the surrounding constructors, the remaining access expressions a_{0} a_{1} ... a_{n} and b_{0} b_{1} ... b_{m} obey:

• either a_{0} ≠ b_{0}

• or for some i such that 0 ≤ i ≤ min(n, m), one of the following conditions hold:

– a_{i} and b_{i} have shapes [x] and [y], respectively, where x and y are different integer constants;

– a_{i} and b_{i} have shapes .f and .g, respectively, where f and g are different record labels.

– a_{i} or b_{i} is a universal any pattern, a 0-ary construction or a literal.

3.1.3 Initialization of variables:

A static sufficient condition ensures that the variables locally declared in processes, or any of their constituents, are initialized before any use. The condition is similar to that used for the same purpose in the Ntif intermediate form, the reader is referred to [7] for details.

3.2 Well-typed programs

3.2.1 Type declarations, type expressions, types

First, it is assumed throughout this section that the constants declared are replaced throughout (in types and expressions) by their values (values of constants can be statically computed), and that the “size” parameters (for queue and array types) and “range” parameters (for interval types) have been computed too (these expressions may only hold constants and literals).

Next, let us distinguish type expressions from types: type expressions may contain user-defined type identifiers, while types may not. Type declarations introduce abbreviations (identifiers) for types or type expressions. With each type expression t, one can clearly associate the type τ obtained from it by recursively replacing type identifiers in t by the type expressions they abbreviate.

Similarly, we will make the same distinction between channel expressions (possibly containing channel identifiers) and channels. With each channel expression p, one can associate the channel π obtained from it by replacing channel identifiers by the channels they abbreviate.

All formal parameters of a process (ports or variables), and local variables, have statically assigned type or channel expressions, in the headers of the process, from which one can compute types or channels as above. By typing context, we mean in the sequel a map that associates:

• with each port, a set made of its attributes (a non empty subset of {in, out}) and a channel. Unless some attribute is made explicit in its declaration, a port has both in and out attributes; • with each shared variable, a set made of its attributes (a nonempty subset of {read, write})

and type. There are no default attributes for variables;

• with each formal parameter, its type;

• with each local variable, its type.

• with each constructor its type. If the constructor is 0-ary, this type is a union type. If it is 1-ary, then that type is a function type τ_{1} → τ_{2}, in which τ_{1} is the type expected for the constructor argument and τ_{2} is the result type of the construction;

Typing contexts are written A in the sequel. A(x) denotes the information (attributes and type(s)) assigned to variable (or port) x in A.

3.2.2 Subtyping

Types obtained as explained above are partially ordered by a relation called subtyping, written ≤ and defined by the following rules:

\frac{τ ∈ \{bool, nat, int\}}{τ ≤ τ} (SU1) \overline{⊥ ≤ τ} (SU2)

\overline{nat ≤ int} (SU3) \frac{x ≥ 0}{x .. y ≤ nat} (SU4) \overline{x .. y ≤ int} (SU5) \frac{x_{1} ≥ x_{2} y_{1} ≤ y_{2}}{x_{1} .. y_{1} ≤ x_{2} .. y_{2}} (SU6)

\frac{τ ≤ τ′}{array k of τ ≤ array k of τ′} (SU7) \frac{τ ≤ τ′}{queue k of τ ≤ queue k of τ′} (SU8)

\frac{\{f_{1}, …, f_{n}\} = \{g_{1}, …, g_{n}\} (∀i, j)(f_{i} = g_{j} ⇒ τ_{i} ≤ τ′_{j})}{record f_{1} : τ_{1}, …, f_{n} : τ_{n} end ≤ record g_{1} : τ′_{1}, …, g_{n} : τ′_{n} end} (SU9)

\frac{\begin{matrix}\{c_{1}^{1}, …, c_{n}^{1}\} = \{c_{1}^{2}, …, c_{m}^{2}\} \\ (∀i, j)(c_{i}^{1} = c_{j}^{2} ⇒ ((i ≤ u ∧ j ≤ v) ∨ (i > u ∧ j > v ∧ τ_{i} ≤ τ′_{j})) \end{matrix}}{union c_{1}^{1} | … | c_{u}^{1} | c_{u+1}^{1} of τ_{u+1} | … | c_{n}^{1} of τ_{n} end ≤ union c_{1}^{2} | … | c_{v}^{2} | c_{v+1}^{2} of τ′_{v+1} | … | c_{m}^{2} of τ′_{n} end} (SU10)

Fields in record types are unordered, as well as variants in union types. In the above rule, constructors are assumed ordered so that those without arguments appear first.

bool and nat types are not related by subtyping, nor are record or union types with different sets of fields or constructors, or arrays or queues of different finite sizes.

The subtyping relation is extended to channels by:

\overline{none ≤ none} (SU11) \frac{τ_{1} ≤ τ′_{1} … τ_{n} ≤ τ′_{n}}{τ_{1}# … #τ_{n} ≤ τ′_{1}# … #τ′_{n}} (SU12)

3.2.3 Typing expressions

A is some typing context, the following rules define the typing relation “:” for expressions.

Subsumption

\frac{A ⊢ E : τ τ ≤ τ′}{A ⊢ E : τ′} (ET1)

Literals

\frac{K ∈ INTEGER V al(K) = k}{A ⊢ K : k .. k} (ET2) \frac{k ∈ \{true, false\}}{A ⊢ k : bool} (ET3)

By abuse of notation, we write K ∈ INTEGER to mean that K belongs to the INTEGER syntactical class. Function V al associates with a token in the INTEGER or NATURAL class the integer it denotes.

Variables, constants and constructions (union values)

\frac{A(X) = \{τ\}}{A ⊢ X : τ} (ET4) \frac{\{read, τ\} ⊆ A(X)}{A ⊢ X : τ} (ET5) \frac{A(C) = \{τ → τ′\} A ⊢ e : τ}{A ⊢ C e : τ′} (ET6)

Shared variables in write-only mode may not be read.

Arithmetic and logical primitives

\frac{A ⊢ x : bool}{A ⊢ not x : bool} (ET7) \frac{A ⊢ x : bool A ⊢ y : bool (@ ∈ \{and, or\})}{A ⊢ x@y : bool} (ET8)

\frac{A ⊢ x : τ τ ≤ int}{A ⊢ −x : τ} (ET9) \frac{A ⊢ x : τ τ′ ≤ τ ≤ int}{A ⊢ $ x : τ′} (ET10)

\frac{A ⊢ x : τ A ⊢ y : τ τ ≤ int (@ ∈ \{+, −, ∗, /, %\})}{A ⊢ x@y : τ} (ET11)

\frac{A ⊢ x : τ A ⊢ y : τ τ ≤ int (@ ∈ \{<, <=, >, >=\})}{A ⊢ x@y : bool} (ET12)

\frac{A ⊢ x : τ A ⊢ y : τ (@ ∈ \{=, <>\})}{A ⊢ x@y : bool} (ET13)

Except for the coercion operator $, arithmetic primitives are homogeneous: their argument(s) and result have the same type. $ converts a numeric value of some type τ ≤ int into a value of some subtype τ′ of τ.

Records

\frac{\{f_{1}, …, f_{n}\} ⊆ Fields A ⊢ l_{1} : τ_{1} … A ⊢ l_{n} : τ_{n}}{A ⊢ \{f_{1} : l_{1}, …, f_{n} : l_{n}\} : record f_{1} : τ_{1}, …, f_{n} : τ_{n} end} (ET14)

\frac{A ⊢ P : record …, f : τ, … end}{A ⊢ P.f : τ} (ET15)

Fields is the set of record field identifiers declared in record types.

Arrays

\frac{A ⊢ k_{1} : τ … A ⊢ k_{n} : τ}{A ⊢ [k_{1}, …, k_{n}] : array of n τ} (ET16)

\frac{A ⊢ P : array of k τ A ⊢ E : 0 .. k−1}{A ⊢ P [E] : τ} (ET17)

Queues

\frac{A ⊢ k_{1} : τ … A ⊢ k_{n} : τ 0 ≤ n ≤ m}{A ⊢ \{|k_{1}, …, k_{n}|\} : queue m of τ} (ET18)

\frac{A ⊢ q : queue of k τ}{A ⊢ empty q : bool} (ET19) \frac{A ⊢ q : queue of k τ}{A ⊢ full q : bool} (ET20)

\frac{A ⊢ q : queue of k τ}{A ⊢ first q : τ} (ET21) \frac{A ⊢ q : queue of k τ}{A ⊢ dequeue q : queue of k τ} (ET22)

\frac{A ⊢ q : queue of k τ A ⊢ E : τ}{A ⊢ enqueue (q, E) : queue of k τ} (ET23) \frac{A ⊢ q : queue of k τ A ⊢ E : τ}{A ⊢ append (q, E) : queue of k τ} (ET24)

3.2.4 Typing patterns

By “pattern”, we mean the left hand sides of assignment statements, or the tuples of variables following “?” in input communication statements.

When used as arguments of some primitive, types of values can be promoted to any of their supertypes (by the use of the subsumption rule), but we want variables of all kinds to only store values of their declared type, and not of larger types. For this reason, patterns cannot be typed like expression.

As an illustrative example, assume variable X was declared with type nat, and array A with type array of 16 int. If lhs of assignments were given types by ⊢, then the statement X := A[2] would be well typed, storing an integer where a natural is expected, since the rhs has type int, and the lhs has type nat, and nat is a subtype of int.

Patterns are given types instead by specific relation “:_{p}”, defined by the following five rules. These rules are similar to those for “:” for variable and access expressions except that subsumption is restricted:

\frac{A(X) = \{τ\}}{A ⊢ X :_{p} τ} (LT1) \frac{\{write, τ\} ⊆ A(X)}{A ⊢ X :_{p} τ} (LT2) \frac{A(C) = \{τ → τ′\} A ⊢ e :_{p} τ}{A ⊢ C e :_{p} τ′} (LT3)

\frac{K ∈ INTEGER A ⊢ K : τ}{A ⊢ K :_{p} τ} (LT4) \frac{k ∈ \{true, false\}}{A ⊢ k :_{p} bool} (LT5) \overline{A ⊢ any :_{p} τ} (LT6)

\frac{A ⊢ P :_{p} array of k τ A ⊢ E : 0 .. k−1}{A ⊢ P [E] :_{p} τ} (LT7)

\frac{A ⊢ P :_{p} record …, f : τ, … end}{A ⊢ P.f :_{p} τ} (LT8)

Shared variables in read-only mode cannot be assigned.

3.2.5 Typing statements, well typed processes

Well-typing of the statement captured in a transition ensures three properties:

(a) That the variables and expressions occurring in the transition are used consistently;

(b) That at most one communication occurs along any possible end-to-end control path of the statement of the transition;

(c) That no shared variable is read of written along any end-to-end control path holding a communication;

As for expressions, some information is infered for statements, assuming a typing context; the “typing” relation for statements is written “:_{s}”; the “types” derived are subsets α of {Shm, Com}. Presence of Shm means that shared storage is manipulated along some control path not performing any communication, presence of Com means that some control path performs a (single) communication but does not read nor writes shared variables. A statement type may hold both Shm and Com, provided shared variables and communications are performed along different control paths.

A process is well-typed if all of its transitions are well-typed in the typing context obtained from its port declarations, formal parameter declarations and local variable declarations. A transition is well typed if the statement it is defined from is well-typed. A statement S is well typed if one can infer S :_{s} α, for some α ⊆ {Shm, Com}, according to the following rules.

The rules make use of an auxiliary predicate Q_{A}(E), holding iff some shared variable occurs in expression E in context A, and of a “conditional” notation b → α | β, standing for α when b holds, or for β otherwise.

Jump, null

\overline{A ⊢ to s :_{s} ∅} (ST1) \overline{A ⊢ null :_{s} ∅} (ST2)

Sequential composition

\frac{A ⊢ S_{1} :_{s} ∅ A ⊢ S_{2} :_{s} α}{A ⊢ (S_{1}; S_{2}) :_{s} α} (ST3) \frac{A ⊢ S_{1} :_{s} α A ⊢ S_{2} :_{s} ∅}{A ⊢ (S_{1}; S_{2}) :_{s} α} (ST4)

\frac{A ⊢ S_{1} :_{s} \{Shm\} A ⊢ S_{2} :_{s} \{Shm\}}{A ⊢ (S_{1}; S_{2}) :_{s} \{Shm\}} (ST5)

Assignments and Case

\frac{A ⊢ P_{1} :_{p} τ_{1} … A ⊢ P_{n} :_{p} τ_{n} A ⊢ E_{1} : τ_{1} … A ⊢ E_{n} : τ_{n}}{A ⊢ P_{1}, …, P_{n} := E_{1}, …, E_{n} :_{s} (∃i ∈ 1..n)(Q_{A}(P_{i}) ∨ Q_{A}(E_{i})) → \{Shm\} | ∅} (ST6)

\frac{A ⊢ P_{1} :_{p} τ_{1} … A ⊢ P_{n} :_{p} τ_{n} A ⊢ E : bool}{A ⊢ P_{1}, …, P_{n} := any where E :_{s} (∃i ∈ 1..n)(Q_{A}(P_{i})) ∨ Q_{A}(E) → \{Shm\} | ∅} (ST7)

\frac{\begin{matrix}A ⊢ P_{1} :_{p} τ … A ⊢ P_{n} :_{p} τ A ⊢ E : τ \\ A ⊢ S_{1} :_{s} α_{1} … A ⊢ S_{n} :_{s} α_{n} (∀i ∈ 1..n)(Q_{A}(P_{i}) ⇒ α_{i} ⊆ \{Shm\}) \end{matrix}}{A ⊢ case e of P_{1} → S_{1} | … | P_{n} → S_{n} end :_{s} α_{1} ∪ ⋯ ∪ α_{n}} (ST8)

Choices and while loop

\frac{A ⊢ E : bool A ⊢ S_{1} :_{s} α_{1} A ⊢ S_{2} :_{s} α_{2} Q_{A}(E) ⇒ α_{1} ∪ α_{2} ⊆ \{Shm\}}{A ⊢ if E then S_{1} else S_{2} end :_{s} α_{1} ∪ α_{2}} (ST9)

\frac{A ⊢ E : bool A ⊢ S :_{s} α Com ∉ α}{A ⊢ while E do S end :_{s} Q_{A}(E) → \{Shm\} | α} (ST10)

\frac{A(v) = \{x .. y\} A ⊢ S :_{s} α Com ∉ α}{A ⊢ foreach v do S end :_{s} Q_{A}(v) → \{Shm\} | α} (ST11)

\frac{A ⊢ S_{1} :_{s} α_{1} … A ⊢ S_{n} :_{s} α_{n}}{A ⊢ select S_{1} [ ] ... [ ] S_{n} end :_{s} α_{1} ∪ ⋯ ∪ α_{n}} (ST12)

if e then s end is handled like if e then s else null end. elsif is handled like else if. Communications \frac{none ∈ A(p)}{A ⊢ p :_{s} \{Com\}} (ST13)

\frac{A ⊢ E_{1} : τ_{1} … A ⊢ E_{n} : τ_{n} \{out, τ_{1}# … #τ_{n}\} ⊆ A(p) ¬(∃i ∈ 1..n)(Q_{A}(E_{i}))}{A ⊢ p ! E_{1}, …, E_{n} :_{s} \{Com\}} (ST14)

\frac{\begin{matrix}A ⊢ X_{1} :_{p} τ_{1} … A ⊢ X_{n} :_{p} τ_{n} A ⊢ E : bool \\ \{in, τ_{1}# … #τ_{n}\} ⊆ A(p) ¬(∃i ∈ 1..n)(Q_{A}(X_{i})) ∨ Q_{A}(E) \end{matrix}}{A ⊢ p ? X_{1}, …, X_{n} where E :_{s} \{Com\}} (ST15)

In an output communication, the tuple of types of the values sent must be a subtype of the channel declared for the port. In an input communication, the channel declared for the port must be a subtype of the tuple of types of the reception pattern.

3.2.6 Well-typed components

Components are checked in a context made of:

• A typing context A, defined as for processes except that locally declared variables all have attributes read and write;

• An interface context I, that associates with all previously declared processes and components an interface of shape ((…, μ_{i}, …), (…, η_{j}, …)), in which μ_{i} is the set of attributes and channel of the i^{th} port declared for the process or component, and η_{j} is the set of attributes and type of the j^{th} formal parameter of the component.

The expressions in components are given types and attributes by relation :_{x}, defined by:

\frac{A(X) = η}{A, I ⊢ X :_{x} η} (CT1) \frac{A ⊢ E : τ (E not a variable)}{A, I ⊢ E :_{x} \{τ\}} (CT2)

A component is well-typed if ok can be inferred for it by relation :_{c}, defined by:

\frac{A, I ⊢ c_{1} :_{c} ok … A, I ⊢ c_{n} :_{c} ok (∀i)(Q_{i} ⊆ Σ(c_{i}))}{A, I ⊢ par Q_{1} → c_{1} || … || Q_{n} → c_{n} end :_{c} ok} (CT3)

The sort Σ(c) of a composition c is computed as follows, according to the structure of c:

Σ(par e_{1} → c_{1} || … || e_{n} → c_{n} end) = Σ(c_{1}) ∪ ⋯ ∪ Σ(c_{2})
Σ(P [q_{1}, …, q_{m}] (v_{1}, …, v_{l}))  = {q_{1}, …, q_{m}}

par … || c_{i} || … end stands for par … || ∅ → c_{i} || … end

par Q in Q_{1} → c_{1} || … || Q_{n} → c_{n} end stands for par (Q ∪ Q_{1}) → c_{1} || … || (Q ∪ Q_{n}) → c_{n} end

If ∗ ∈ Q, then Q → c is handled like Σ(c) → c.

\frac{A ⊢ e_{1} :_{x} η_{1} … A ⊢ e_{n} :_{x} η_{n} ((A(p_{1}), …, A(p_{n})), (η_{1}, …, η_{m})) ≺ I(C)}{A, I ⊢ C [p_{1}, …, p_{n}] (e_{1}, …, e_{m}) :_{c} ok} (CT4)

Where ((μ_{1}^{1}, …, μ_{n_{1}}^{1}), (η_{1}^{1}, …, η_{m_{1}}^{1})) ≺ ((μ_{1}^{2}, …, μ_{n_{2}}^{2}), (η_{1}^{2}, …, η_{m_{2}}^{2})) holds iff:

• n_{1} = n_{2} and for each i: μ_{i}^{2} ⊆ μ_{i}^{1} ∧ μ_{i}^{1} − μ_{i}^{2} ⊆ {in, out}

• m_{1} = m_{2} and for each j: if {read, write}∩η_{j}^{2} ≠ ∅ then η_{j}^{2} ⊆ η_{j}^{1} else τ_{j}^{1} ≤ τ_{j}^{2} where η_{j}^{1} = {τ_{j}^{1}} and η_{j}^{2} = {τ_{j}^{2}} 3.2.7 Well typed programs

A program is well typed if the declarations and component instance it contains are well typed.

3.3 Choosing types for expressions

Expressions may have in general several types: arithmetic expressions typically have several types, resulting from the subtyping rules of arithmetics, the empty queue constant {| |} has any queue type.

The typing rules and method explained in section 3.2 ensure that all expressions in some program can be given at least one type such that the whole program is well-typed.

Now, as will be seen, the semantics of arithmetic operations depends on their type, which is why it is necessary to explain the rules leading to a choice of a particular type for arithmetic primitives and constants when several types are admissible.

The rule retained is the following: when several types are admissible for an expression, the Fiacre typechecker assigns to it the largest (by the subtyping relation) type possible permitted by the context. If no such largest type is implied by the context, then the expression is rejected (considered ill-typed).

As an illustrative example, consider the following statements, with the assumption that the enclosing process or component holds the declarations x : 0..255, y : int, q : queue 5 of nat:

1. y := x + 5

Pattern y has type int, expression x has any supertype of 0..255. Hence, expression x + 5 has all types which are subtypes of int and supertypes of 0..255; type int will be selected;

2. x := x + 5

Expression x + 5 admits a single type: 0..255;

3. if x > 1000 then...

The arguments of > are only required to be subtypes of int, hence both that instance of x and constant 1000 are assigned type int;

4. if q = {| |} then...

Similarly, constant {| |} has here the type of q : queue 5 of nat;

5. if {| |} = {| |} then...

The context does not provide any upper bound for the types of the empty queue constants, hence this statement is rejected.

In the next Section, overloaded primitives whose interpretation depends on their type are assumed annotated with an indication of the type chosen by the above method. This concerns arithmetic primitives (annotated by the type of their(s) argument(s)) and queues primitives (annotated by the type of their queue argument).

4 Timed operational semantics

All programs in this section are assumed well-formed and well-typed. Declared constants are assumed replaced throughout by their statically computed values. Overloaded primitives are assumed annotated as explained in Section 3.3.

4.1 Semantics of expressions

4.1.1 Semantic domains The semantics of expressions is given in denotational style, it associates with every well-typed expression a value in some mathematical domain D built as follows. Let ZZ and IN be the set of integers and non-negative integers, respectively, equipped with their

usual arithmetic and comparison functions;

B = {true, false} be a domain of truth values, equipped with functions not, and and or; S be the set of finite strings containing letters, digits, and symbol ’ ’; Arrays(E) be the set of mappings from finite subsets of IN to E; Records(E) be set of mappings from finite subsets of S to E;

Then D = D_{ω}, where: D_{0} = ZZ ∪ B ∪ S D_{n+1} = D_{n} ∪ Arrays(D_{n}) ∪ Records(D_{n})

Fiacre arithmetic expressions are given meanings in set ZZ, boolean expressions in B, arrays in some set Arrays(D_{n}), union constants as strings, tagged unions and records in some set Records(D_{n}), for some finite n, all subsets of D. Queues denote some elements of Arrays(D_{n}). The following mappings are defined for queue denotations (D(m) is the domain of mapping m):

• empty q is equal to true if D(q) = ∅, or false otherwise;

• full k q (n ∈ IN) is equal to true if k − 1 ∈ D(q), or false otherwise;

• first q = q(0), assuming 0 ∈ D(q);

• dequeue q, assuming 0 ∈ D(q), is the mapping q′ such that q′(x − 1) = q(x) for all x ∈ D(q);

• enqueue q e is the mapping q′ such that q′(x) = q(x) for x ∈ D(q), and q′(a) = e, where a is the smallest non negative integer not in D(q).

• append q e is the mapping q′ such that q′(0) = e and q′(x + 1) = q(x) for x ∈ D(q).

4.1.2 Stores Expression are given meanings relative to a store. The store associates values in D with (some) variables. Stores are written e, e′, etc, e(x) is the value associated with variable x in store e, D(e) is the domain of e.

4.1.3 Semantic rules for expressions

Evaluation rules all have the following shape. The rule means that, under conditions P_{1} to P_{n}, the value of expression E with store e is v. The store e may be omitted if the result does not depend on its contents.

\frac{P_{1} … P_{n}}{e ⊢ E ⇝ v}

Core expressions

• Numeric constants denote integers in ZZ. Implementations may choose to reject literals that are not machine representable;

• 0-ary constructors (union constants) denote strings in S;

• The booleans true and false denote values true and false in B, respectively;

• Representing mappings by their graphs, records, arrays and queues are given meanings by:

\frac{⊢ l_{1} ⇝ v_{1} … ⊢ l_{n} ⇝ v_{n}}{⊢ [l_{1}, …, l_{n}] ⇝ \{(0, v_{1}), …, (n − 1, v_{n})\}} (ES1)

\frac{⊢ l_{1} ⇝ v_{1} … ⊢ l_{n} ⇝ v_{n}}{⊢ \{f_{1} : l_{1}, …, f_{n} : l_{n}\} ⇝ \{(f_{1}, v_{1}), …, (f_{n}, v_{n})\}} (ES2)

\overline{⊢ \{| |\} ⇝ ∅} (ES3) \frac{⊢ l_{1} ⇝ v_{1} … ⊢ l_{n} ⇝ v_{n}}{⊢ \{|l_{1}, …, l_{n}|\} ⇝ \{(0, v_{1}), …, (n − 1, v_{n})\}} (ES4)

• 0-ary constructors (union constants) denote strings in S, constructions denote pairs in S × D.

\overline{e ⊢ C ⇝ |C|} (ES5) \frac{e ⊢ E ⇝ v}{e ⊢ C E ⇝ \{(|C|, v)\}} (ES6)

|C| ∈ S the name of the constructor.

Given a value v and a pattern P, the matching predicate M(v, P), read “v matches P ” is defined as follows, according to the structure of P (C is a constructor):

M((c, v), C P) iff c ∈ S ∧ c = |C| ∧ M(v, P)

M(c, C) iff c ∈ S ∧ c = |C|

M(l, L) iff ⊢ L ⇝ l (L is a numeric or boolean literal) M(v, X) true (X is a variable or an access pattern)

• Variables evaluate to the values they are bound to in the store. Non initialized or partially initialized variables are not in the stores, hence the condition on domains. Satisfaction of these conditions is guaranteed by the static semantic constraints explained in Section 3.1.3.

\frac{X ∈ D(e)}{e ⊢ X ⇝ e(X)} (ES7)

• Array and record access evaluate the obvious way (arrays are indexed from 0). Well-typing ensures that array indices, when their evaluation succeed, cannot be out of range, nor fields undefined in the records they are sought for.

\frac{e ⊢ P ⇝ a e ⊢ E ⇝ i i ∈ D(a)}{e ⊢ P [E] ⇝ a(i)} (ES8) \frac{e ⊢ P ⇝ r f ∈ D(r)}{e ⊢ P.f ⇝ r(f)} (ES9)

• Conditional expressions are given meanings as follows:

\frac{e ⊢ E_{c} ⇝ true e ⊢ E_{1} ⇝ v}{e ⊢ E_{c} ? E_{1} : E_{2} ⇝ v} (ES10) \frac{e ⊢ E_{c} ⇝ false e ⊢ E_{2} ⇝ v}{e ⊢ E_{c} ? E_{1} : E_{2} ⇝ v} (ES11)

Primitives

Well-typing implies that all primitives in an expression can be assigned at least one type. When several types can be assigned to some primitive, the typechecker is assumed to have computed a suitable one for it, typically the type that puts the weakest constraints on the arguments of the primitive (see Section 3.3). The primitives whose semantics is type-dependent appear in the semantic rules with type annotations added (by the typechecker).

Some primitives are partially defined (e.g. arithmetic functions over intervals, or taking an element from a queue). This appears in the rules by some extra hypothesis (side-conditions). The rules do not make precise any exception handling mechanism, it is assumed that implementations are able to detect when a rule is not applicable and take an adequate decision in that case.

• Arithmetic primitives at type τ (τ is some subtype of int):

\frac{e ⊢ x ⇝ a In(−a, τ)}{e ⊢ −_{τ} x ⇝ −a} (ES12) \frac{e ⊢ x ⇝ a e ⊢ y ⇝ b In(a @ b, τ) @ ∈ \{+, −, ∗\}}{e ⊢ x @_{τ} y ⇝ a @ b} (ES13)

\frac{e ⊢ x ⇝ a In(a, τ)}{e ⊢ $_{τ} x ⇝ a} (ES14)

\frac{e ⊢ x ⇝ a e ⊢ y ⇝ b b ≠ 0 In(a @ b, τ) @ ∈ \{/, %\}}{e ⊢ x @_{τ} y ⇝ a @ b} (ES15)

Operations over nat or interval types behave like those over int type except that they are undefined if the result is not in the expected set. Predicate In is defined as follows: In(v, int) always holds, In(v, nat) holds if v ≥ 0, and In(v, a..b) if a ≤ v ≤ b. Implementations may strengthen predicate In by conditions asserting that the results are machine representable.

• Boolean primitives:

\frac{e ⊢ x ⇝ a}{e ⊢ not x ⇝ not a} (ES16) \frac{e ⊢ x ⇝ a e ⊢ y ⇝ b}{e ⊢ x and y ⇝ a and b} (ES17) \frac{e ⊢ x ⇝ a e ⊢ y ⇝ b}{e ⊢ x or y ⇝ a or b} (ES18)

Boolean operators are evaluated functionally. Lazy boolean operators can be implemented with conditional expressions.

• Comparison and equality (@ ∈ {<, >, <=, >=, =, <>}):

\frac{e ⊢ x ⇝ a e ⊢ x ⇝ b a @ b}{e ⊢ x @ y ⇝ true} (ES19) \frac{e ⊢ x ⇝ a e ⊢ x ⇝ b ¬(a @ b)}{e ⊢ x @ y ⇝ false} (ES20)

• Primitives for queues at type τ (a queue type)

Assuming τ is some queue type queue N of τ′, Cap(τ) denote capacity N.

\frac{e ⊢ q ⇝ Q}{e ⊢ empty q ⇝ empty Q} (ES21) \frac{e ⊢ q ⇝ Q}{e ⊢ full_{τ} q ⇝ full (Cap(τ)) Q} (ES22)

\frac{e ⊢ q ⇝ Q D(Q) ≠ ∅}{e ⊢ first q ⇝ first Q} (ES23) \frac{e ⊢ q ⇝ Q D(Q) ≠ ∅}{e ⊢ dequeue q ⇝ dequeue Q} (ES24)

\frac{e ⊢ q ⇝ Q e ⊢ x ⇝ v Cap(τ) − 1 ∉ D(Q)}{e ⊢ enqueue_{τ} (q, x) ⇝ enqueue Q v} (ES25)

\frac{e ⊢ q ⇝ Q e ⊢ x ⇝ v Cap(τ) − 1 ∉ D(Q)}{e ⊢ append_{τ} (q, x) ⇝ append Q v} (ES26)

first and dequeue are undefined on empty queues. enqueue_{τ} and append_{τ} are undefined on full queues (already holding Cap(τ) elements).

4.1.4 Patterns

Left-hand sides of assignments evaluate to pairs (z, g), in which z is a value and g maps values to stores. Intuitively, g(v), where v is the value put into the location referred to by the lhs, is the updated store; z at some level is a partial value used to compute function g at the level above.

The evaluation relation for lhs of assignments is denoted ⇝^{l} and defined by the following rules, in which:

• (λv. f(v)) is the mapping that, applied to value v, returns the value mapped by f to v;

• extend f x = f x if x ∈ D(f), or ∅ otherwise;

• [x_{1} ↦ v_{1}, …, x_{n} ↦ v_{n}] ⊕ e is the function f such that f(x_{i}) = v_{i} for any i ∈ 1..n, and f(z) = e(z) for any z ∈ D(e) − {x_{1}, …, x_{n}}.

\overline{e ⊢ X ⇝^{l} (extend e X), (λv. [X ↦ v] ⊕ e)} (LS1)

\frac{e ⊢ P ⇝^{l} e′, a e ⊢ E ⇝ i}{e ⊢ P [E] ⇝^{l} (extend e′ i), (λv. a([i ↦ v] ⊕ e′))} (LS2)

\overline{e ⊢ C ⇝^{l} ∅, e} (LS3)

Where C is a literal (numeric or boolean constant) or a 0-ary constructor.

\frac{e ⊢ P ⇝^{l} e′, r}{e ⊢ C P ⇝^{l} e′, r} (LS4)

Where C is a 1-ary constructor.

4.2 Semantics of Processes

4.2.1 Semantics of statements The semantics of statements is expressed operatioally by a labelled relation. The relation holds triples (S, e) ⟹^{l} (S′, e′) in which:

• S is a statement;

• e, e′ are stores;

• S′ ∈ {done} ∪ {target s|s ∈ Λ}, where Λ is the declared set of states of the process;

• l is either a communication action or the silent action ϵ. Communication actions are sequences p v_{1} … v_{n}, in which p is a port and v_{1} … v_{n} (n ≥ 0) are values.

Relation ⟹^{l} is defined inductively from the structure of statements, by the following rules. To, null

\overline{(to s, e) ⟹^{ϵ} (target s, e)} (SS1) \overline{(null, e) ⟹^{ϵ} (done, e)} (SS2)

Deterministic assignment

\frac{\begin{matrix}\begin{matrix}e ⊢ E_{1} ⇝ v_{1} \\ e ⊢ P_{1} ⇝^{l} e_{1}, a_{1} \\ M(v_{1}, P_{1}) \end{matrix} & \begin{matrix}e ⊢ E_{2} ⇝ v_{2} \\ a_{1}(v_{1}) ⊢ P_{2} ⇝^{l} e_{2}, a_{2} \\ M(v_{2}, P_{2}) \end{matrix} & . . . . . . . . . & \begin{matrix}e ⊢ E_{n} ⇝ v_{n} \\ a_{n−1}(v_{n−1}) ⊢ P_{n} ⇝^{l} e_{n}, a_{n} \\ M(v_{n}, P_{n}) \end{matrix} \\ e′ = a_{n}(v_{n}) \end{matrix}}{(P_{1}, P_{2}, …, P_{n} := E_{1}, E_{2}, …, E_{n}, e) ⟹^{ϵ} (done, e′)} (SS3)

The independence property for accesses in multiple assignments, enforced by the static semantic constraint in Section 3.1.2, ensures that the resulting store is invariant by any permutation of accesses P_{1}, …, P_{n} and the corresponding expressions E_{1}, …, E_{n}.

Nondeterministic assignment

\frac{\begin{matrix}e ⊢ P_{1} ⇝^{l} e_{1}, a_{1} \\ e′ = a_{n}(v_{n}) \end{matrix} \begin{matrix}a_{1}(v_{1}) ⊢ P_{2} ⇝^{l} e_{2}, a_{2} \\ [e′ ⊢ E ⇝ true] \end{matrix} … a_{n−1}(v_{n−1}) ⊢ P_{n} ⇝^{l} e_{n}, a_{n}}{(P_{1}, P_{2}, …, P_{n} := any [where E], e) ⟹^{ϵ} (done, e′)} (SS4)

v_{i} ranges over all values of the type of P_{i} (necessarily a boolean or numeric type).

While, foreach

\frac{e ⊢ E ⇝ true (S; while E do S end, e) ⟹^{l} (S′, e′)}{(while E do S end, e) ⟹^{l} (S′, e′)} (SS5)

\frac{e ⊢ E ⇝ false}{(while E do S end, e) ⟹^{ϵ} (done, e)} (SS6)

It is assumed that condition E eventually evaluates to false.

\frac{(V := v_{1} ; S ; … V := v_{n} ; S, e) ⟹^{l} (S′, e′)}{(foreach V do S end, e) ⟹^{l} (S′, e′)} (SS7)

Where v_{1}, …, v_{n} is the set of values of interval type V, in increasing order. Deterministic choice

\frac{e ⊢ E ⇝ true (S_{1}, e) ⟹^{l} (S, e′)}{(if E then S_{1} else S_{2} end, e) ⟹^{l} (S, e′)} (SS8) \frac{e, E ⇝ false (S_{2}, e) ⟹^{l} (S, e′)}{(if E then S_{1} else S_{2} end, e) ⟹^{l} (S, e′)} (SS9)

if e then s end is handled like if e then s else null end. elsif is handled like else if. Case

\frac{e ⊢ E ⇝ v M(v, P_{1}) (P_{1} := E ; S_{1}, e) ⟹^{l} (S′, e′)}{(case E of P_{1} → S_{1} | ... | P_{n} → S_{n} end, e) ⟹^{l} (S′, e′)} (SS10)

\frac{e ⊢ E ⇝ v ¬M(v, P_{1}) (case E of P_{2} → S_{2} | ... | P_{n} → S_{n} end, e) ⟹^{l} (S′, e′)}{(case E of P_{1} → S_{1} | ... | P_{n} → S_{n} end, e) ⟹^{l} (S′, e′)} (SS11)

Nondeterministic choice

\frac{(S_{i}, e) ⟹^{l} (S′, e′)}{(select S_{1} [ ] ... [ ] S_{n} end, e) ⟹^{l} (S′, e′)} (SS12)

Sequential composition

\frac{(S_{1}, e) ⟹^{l} (target s, e′)}{(S_{1}; S_{2}, e) ⟹^{l} (target s, e′)} (SS13) \frac{(S_{1}, e) ⟹^{l_{1}} (done, e′) (S_{2}, e′) ⟹^{l_{2}} (S′, e′′)}{(S_{1}; S_{2}, e) ⟹^{l_{1}.l_{2}} (S′, e′′)} (SS14)

with “.” such that ϵ.ϵ = ϵ and ϵ.l = l.ϵ = l, for any l. The well-formedness condition implies l_{1} = ϵ ∨ l_{2} = ϵ. Note that the statements following a to statement are dead code.

Communication

\overline{(p_{τ} , e) ⟹^{p} (done, e)} (SS15)

\frac{e ⊢ E_{1} ⇝ v_{1} … e ⊢ E_{n} ⇝ v_{n}}{(p!E_{1}, …, E_{n}, e) ⟹^{p v1 ... vn} (done, e)} (SS16)

\frac{\begin{matrix}e ⊢ P_{1} ⇝^{l} e_{1}, a_{1} \\ e′ = a_{n}(v_{n}) \end{matrix} \begin{matrix}a_{1}(v_{1}) ⊢ P_{2} ⇝^{l} e_{2}, a_{2} \\ [e′ ⊢ E ⇝ true] \end{matrix} … a_{n−1}(v_{n−1}) ⊢ P_{n} ⇝^{l} e_{n}, a_{n}}{(p?P_{1}, P_{2}, .., P_{n} [where E], e) ⟹^{p v_{1} ... v_{n}} (done, e′)} (SS17)

v_{i} ranges over all values of the type of P_{i}.

4.2.2 Process configurations, initial process configurations

A process configuration is a pair (s, e) constituted of a process state s and a store e capturing the values of all variables referred to in the process. Each process has a set of initial configurations, obtained as follows:

• Let s_{0} be a store capturing the values for all parameters and local variables of the process, given their actual declared values. If some variable was not initialized in its declaration, then any value can be chosen for it in s_{0} (e.g. ∅) as the “well-initialized” condition explained in Section 3.1.3 guarantees that this default value will not be used;

• Then:

– If the process has no init statement, it admits a single initial configuration: (s_{0}, e_{0}), in which s_{0} is the source state of the first transition of the process;

– If the process has an init statement S_{i} then, from the static restrictions put upon init statements, (S_{i}, e_{0}) necessarily evaluates by ⟹^{ϵ} to some pair (target s, e). Each such (target s, e) defines a possible initial configuration (s, e) for the process.

4.3 Semantics of components

The semantics, or behavior, of a component is a Timed Transition System. These are Labelled Transition Systems extended with state properties and time-elapsing transitions. The semantics of a component is obtained compositionally from the semantics of the process instances and component instances it captures and the composition operator. Priority and timing constraints possibly restrict the result of compositions. Finally, some ports may be made local to the component, preventing further interactions through these.

4.3.1 Component configurations, terminology

Abstract components: Consider the following grammar of abstract components:

c ::= hide H c  hiding
| prio Π c  priority
| c′  composition
c′ ::= par g_{1} → c′_{1} || … || g_{2} → c′_{2} end composition
| comp Φ F (c, a)  component instance
| proc Φ F (s, a)  process instance

Any Fiacre component will be represented by an abstract term of the form: hide H (prio Π c), in which c is some term involving only compositions and instances. In this term:

• H maps port labels to time intervals (default [0, ∞)), as made explicit in the local port declaration of the component, if any;

• Π is the priority relation, translating the priorities declared in the process, if any;

Compositions are assumed “normalized”: stars and factorized port sets are eliminated as explained in Section 3.2.6. The leaves of compositions are component instances comp Φ F (c, a) or process instances proc Φ F (s, a), in which:

• A process or component instance interacts through the ports passed as arguments to it. Φ is a port substitution, mapping the ports declared in the header of the process or component to those passed as arguments. Substitution Φ is extended to communication action by:

Φ(ϵ) = ϵ

Φ(p v_{1} … v_{n}) = (Φ p) v_{1} … v_{n}

• (c, a) in comp Φ F (c, a) is an abstract component and a store. F is a function that, given the variables of the component passed as references to the instance, renames these so that they bear the names they have in the instance body.

• (s, a) in proc Φ F (s, a) is a process configuration. F is defined as for component instances.

Interactions: For any communication action l, let us define L(l) by:

L(ϵ) = ϵ

L(p v_{1} … v_{n}) = p

Then, assuming transition (from s S) is among those of a process, the enabled interactions of that process at configuration (s, e) is the set:

Ω(s, e) = {L(l) | (∃s′, e′, l)((S, e) ⟹^{l} (target s′, e′))}

Components are typically defined as products of process instances and/or other components, hence process interactions are typically products of process or component interactions. Abstractly, component interactions obey the following syntax, in which symbol • is used to mean that a particular subcomponent does not participate in an interaction:

k ::= ϵ  silent process interaction
| p  labelled process interaction
| (k′_{1}, …, k′_{n}) product interaction, for any n >= 2
k′ ::= •  not involved
| k  component interaction

An interaction is independant from another, written k ι k′, if the sets of subcomponents they respectively involve (the indices of their members distinct from •) are disjoints.

Component configurations, initial component configurations Component configurations are triples (c, e, ψ) in which c is an abstract component, as defined in Section 4.3.1, e is a store, and ψ is a function called the interaction environment. Function ψ maps component interactions at that configuration to a time interval and a communication label or ϵ.

As for processes, the values of the parameters passed to a process, of its local variables, and possibly its initialization statement defines its initial store s_{0}. A component may admit several initial stores.

The initial configurations of a component all have the shape of the abstract component, in which abstract process instances proc Φ F (s, a) capture an initial configuration of the process and abstract component instances comp Φ F (c, a) capture an initial abstract state and initial store of the subcomponent.

4.3.2 Semantic rules for components

The labelled semantics relation, linking component configurations, has two sorts of transitions: discrete (⟶_{k}^{l}, specifying a communication action and an interaction) and continuous (time elapse

transitions ⟶^{θ} where θ is some nonnegative real number).

Continuous transitions

\frac{(∀k ∈ D(ψ))(θ ≤ ↑ψ(k))}{(c, e, ψ) ⟶^{θ} (c, e, ψ − . θ)} (PS1)

Time may elapse as long as no time-constrained interaction overflows its deadline.

For any interval r, ↑ r is its right endpoint, or ∞ if r is not right-bounded.

For any k: (ψ − . θ)(k) = (I, b) where I = {x−θ | (x−θ) ≥ 0∧x ∈ I′} and (I′, b) = ψ(k).

Discrete Transitions

Compositions

For any abstract composition c = par g_{1} → c_{1} || … || g_{n} → c_{n} end with n components and any A = {a_{1}, …, a_{m}} ⊆ {1, …, n}, let c[g_{a_{1}} → c_{a_{1}}, …, g_{a_{m}} → c_{a_{m}}]_{A}^{n} denote the result of replacing the components of c indexed over A by those made explicit between the brackets.

Similarly, given a product ψ = ψ_{1} × ⋯ × ψ_{n} of n interaction environments (soon to be defined) and A ⊆ {1, …, n}, ψ[ψ_{a_{1}}, …, ψ_{a_{m}}]_{A}^{n} will denote ψ in which the members indexed over A are replaced by those between the brackets, respectively.

Finally, let us denote •[k_{a_{1}}, …, k_{a_{m}}]_{A}^{n} a product of n interactions all of them being • except those indexed over A which have the values shown between the brackets.

The semantics of compositions is then defined by the following two rules:

\frac{(c′, e′, ψ′) ⟶_{k}^{l} (c′′, e′′, ψ′′) l = ϵ ∨ L(l) ∉ g}{(c[g → c′]_{\{i\}}^{n}, e′, ψ[ψ′]_{\{i\}}^{n}) ⟶_{•[k]_{\{i\}}^{n}}^{l} (c[g → c′′]_{\{i\}}^{n}, e′′, ψ[ψ′′]_{\{i\}}^{n})} (PS2)

\frac{(∀j ∈ A)((c_{j}, e, ψ_{j}) ⟶_{k_{j}}^{p v_{1} ... v_{k}} (c′_{j}, e, ψ′_{j}) (∀i ∈ \{1, …, n\})(c = c[(g ∪ \{p\}) → c′]_{\{i\}}^{n} ⇒ i ∈ A)}{\begin{aligned}& (c[g_{a_{1}} → c_{a_{n}}, …, g_{a_{m}} → c_{a_{m}}]_{A}^{n}, e, ψ[ψ_{a_{1}}, …, ψ_{a_{m}}]_{A}^{n}) \\ ⟶_{•[k_{a_{1}},...,k_{am}]_{A}^{n}}^{p v_{1} ... v_{k}} & (c[g_{a_{1}} → c′_{a_{1}}, …, g_{a_{m}} → c′_{a_{m}}]_{A}^{n}, e, ψ[ψ′_{a_{1}}, …, ψ′_{a_{m}}]_{A}^{n}) \end{aligned}} (PS3)

Where the product ψ_{1} × ⋯ × ψ_{n} of n interaction environments is defined as follows, depending on the guards g_{i} in the composition operator:

{(•[k]_{{i}}^{n}, (r, b))  | (k, (r, b)) ∈ ψ_{i} ∧ (b = ϵ ∨ b ∉ g_{i})}
∪ {(•[k_{a_{1}}, …, k_{a_{m}}]_{A}^{n}, (r, b)) | (∀j ∈ A)((k_{j}, (r, b)) ∈ ψ_{j} ∧ b ∈ g_{j}) ∧
(∀i ∈ {1, …, n})(b ∈ g_{i} ⇒ i ∈ A)}

Intuitively, the domain of ψ_{1} × ⋯ × ψ_{n} is the set of possible interactions of the composition, built from the interactions of the subcomponents and the particular composition operator. Note in this rule that the store does not change; well-typing implies that the store may only change on silent transitions.

Hiding

\frac{(c, e, Relax_{H} ψ) ⟶_{k}^{l} (c′, e′, ψ′) L(l) ∉ D(H)}{(hide H c, e, Hide_{H} ψ) ⟶_{k}^{l} (hide H c′, e′, Hide_{H} ψ′)} (PS4)

Where Relax_{H} relaxes the intervals of interactions labelled in D(H) and Hide_{H} makes these interactions silent. Formally:

Relax_{H} ψ = {(k, (r, b)) ∈ ψ | b ∉ D(H)}
∪ {(k, ([0, ∞), b)) | b ∈ D(H) ∧ (∃r)((k, (r, b)) ∈ ψ)}
Hide_{H} ψ = {(k, (r, b)) ∈ ψ | b ∉ D(H)}
∪ {(k, (r, ϵ)) | (∃r)(∃b ∈ D(H))((k, (r, b)) ∈ ψ)}

\frac{(c, e, Relax_{H} ψ) ⟶_{k}^{p v_{1} ... v_{n}} (c′, e′, ψ′) p ∈ D(H) 0 ∈ E where (E, b) = ψ(k)}{(hide H c, e, Hide_{H} ψ) ⟶_{k}^{ϵ} (hide H c′, e′, Hide_{H} (Reset_{H} ψ′))} (PS5)

Where Reset_{H} ψ′ sets the intervals of the “newly enabled” interactions (those not independant from k) having their label in D(H). Formally:

\begin{aligned}Reset_{H} ψ & = & \{(k′, (r, b)) ∈ ψ | k′ ι k ∨ b ∉ D(H)\} \\ & ∪ & \{(k′, (H b, b)) | k′ ι̸ k ∧ b ∈ D(H) ∧ (∃r)((k′, (r, b)) ∈ ψ)\} \end{aligned}

Discrete transitions must be possible without additional delay.

Priorities

\frac{(c, e, ψ) ⟶_{k}^{l} (c′, e′, ψ′) (∀l′, k′, b)((c, e, ψ) ⟶_{k′}^{l′} b ⇒ (L(l′), L(l)) ∉ Π)}{(prio Π c, e, ψ) ⟶_{k}^{l} (prio Π c′, e′, ψ′)} (PS6)

Priorities over labels induce priorities over interactions. An interaction may not occur when some other interaction with higher priority is possible. Priorities never relate silent interactions.

Component instance

\frac{(c, F e_{s} ∪ a, ψ) ⟶_{k}^{l} (c′, F e′_{s} ∪ a′, ψ′)}{(comp Φ F (c, F e_{s} ∪ a), e_{s} ∪ e, R Φ ψ) ⟶_{k}^{Φ(l)} (comp Φ F (c′, F e′_{s} ∪ a′), e′_{s} ∪ e, R Φ ψ′)} (PS7)

Where R Φ ψ = {(r, Φ(b)) | (r, b) ∈ ψ}

The store of the component makes explicit the entries corresponding to the variables passed to the component instance by reference (e_{s}) (those passed by value have been captured when determining the initial configuration). Those entries appear in the store of the instance renamed according to function F (see Section 4.3.1).

Process instance

\frac{(S, F e_{s} ∪ a) ⟹^{l} (target s′, F e′_{s} ∪ a′) (from s S) ∈ T ψ′ = \{(k, ([0, ∞), Φ(k))) | k ∈ Ω(s′, F e′_{s} ∪ a′)\}}{(proc Φ F (s, F e_{s} ∪ a), e_{s} ∪ e, ψ) ⟶_{L(l)}^{Φ(l)} (proc Φ F (s′, F e′_{s} ∪ a′), e′_{s} ∪ e, ψ′)} (PS8)

Where:

• T is the set of transitions of the process;

• Ω(s, e) is the set of interactions enabled at configuration (s, e) in the process (see Section 4.3.1);

• Stores are handled exactly as in the rule for component instances.

The interval function at the target configuration associates interval [0, ∞) and label Φ(k) with each enabled interaction k.

4.4 Semantics of programs

A program is a series of declarations followed by a component or process identifier. The semantics of a program is the semantics of the process or component denoted by that identifier.

References

[1] A. Basu, M. Bozga, and J. Sifakis. Modeling heterogeneous real-time systems in BIP. In 4th IEEE International Conference on Software Engineering and Formal Methods (SEFM06), Pune, pages 3–12, September 2006.

[2] B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. on Software Engineering, 17(3):259–273, 1991.

[3] B. Berthomieu, P.-O. Ribet, and F. Vernadat. The tool tina – construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research, 42-No 14, 2004.

[4] B. Berthomieu, P.-O. Ribet, F. Vernadat, J. Bernartt, J.-M. Farines, J.-P. Bodeveix, M. Filali, G. Padiou, P. Michel, P. Farail, P. Gaufillet, P. Dissaux, and J.-L. Lambert. Towards the verification of real-time systems in avionics: the Cotre approach. In Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems FMICS’2003, (Trondheim, Norway), volume 80 of Electronic Notes in Theoretical Computer Science, pages 201–216. Elsevier, June 2003. Also published as Rapport LAAS Nr. 03185.

[5] Mamoun Filali, Frédéric Lang, Florent Péres, Jan Stoecker, and François Vernadat. Modèles pivots pour la reprśentation des processus concurrents asynchrones, February 2007. Délivrable n^{o} 4.2.3 du projet ANR05RNTL03101 OpenEmbeDD.

[6] Hubert Garavel. On the introduction of gate typing in E-LOTOS. In Piotr Dembinski and Marek Sredniawa, editors, Proceedings of the 15th IFIP International Workshop on Protocol Specification, Testing and Verification (Warsaw, Poland). IFIP, Chapman & Hall, June 1995.

[7] Hubert Garavel and Frédéric Lang. NTIF: A general symbolic model for communicating sequential processes with data. In Doron Peled and Moshe Vardi, editors, Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE’2002 (Houston, Texas, USA), volume 2529 of Lecture Notes in Computer Science, pages 276–291. Springer Verlag, November 2002. Full version available as INRIA Research Report RR-4666.

[8] Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. Cadp 2006: A toolbox for the construction and analysis of distributed processes. In Proceedings of the 19th International Conference on Computer Aided Verification CAV’07 (Berlin, Germany), 2007.

[9] Hubert Garavel and Mihaela Sighireanu. A graphical parallel composition operator for process algebras. In Jianping Wu, Qiang Gao, and Samuel T. Chanson, editors, Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE/PSTV’99 (Beijing, China), pages 185–202. IFIP, Kluwer Academic Publishers, October 1999.

[10] ISO/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization — Information Technology, Genève, September 2001.

[11] P. M. Merlin and D. J. Farber. Recoverability of communication protocols: Implications of a theoretical study. IEEE Tr. Comm., 24(9):1036–1043, Sept. 1976.

[12] Mihaela Sighireanu. Contribution à la définition et à l’implémentation du langage “Extended LOTOS”. Thèse de doctorat, Université Joseph Fourier (Grenoble), January 1999.

[13] Mihaela Sighireanu. LOTOS NT user’s manual (version 2.1). INRIA projet VASY.

    ftp://ftp.inrialpes.fr/pub/vasy/traian/manual.ps.Z, November 2000.