Julien Deantoni

Papa Issa Diallo

Joel Champeau

Benoit Combemale

Ciprian Teodorov

Operational Semantics of the Model of Concurrency and Communication Language

Keywords: Operational semantics, meta language, MoC, language semantics, concurrency Sémantique opérationnelle, meta langage, MoC, sémantique, concurrence

In the GEMOC project, moccml is dedicated to define the concurrency model associated with the DSMLs. The purpose of this document is to define the operational semantics of the moccml language and also to define the first steps of an approach to provide an exhaustive exploration of the moccml models. This document presents the operational semantics of the moccml language. The chapter is divided in several sections that present the grammar rules of the language and the operational rules mainly defined using mathematical grounds and Plotkin [2] rules. Chapter 3 presents the elements that are relevant to describe the evolution of a moccml model. Chapter 4 presents a draft of how exhaustive exploration is to be realized in a context using moccml models. Finally Chapter 5 presents the conclusion.

Introduction

Purpose

The moccml language is a new formalism to express behavioral semantics of DSLs based on the Model of Computation (MoC) theory. The Metamodel of the language defines concepts to model constraints that control the execution of an application model according to formal execution rules. The modeled constraints are expressed in the form of relations between clocks representing relevant events of the system. As such, the language takes advantage from the ccsl formalism which defines constraints on clocks, and from an operational mechanism of relation description based on finite state automata.

The general idea of adding behavioral semantics to DSLs is driven by the motivation to provide executable models and to make explicit their concurrency model. In order to perform analysis (e.g.,by simulation or model-checking), not only the models should be executable, but also their concurrency model should be explicit and formal.

In practice, the executability and concurrency models are covered by the description of the execution semantics of DSMLs, whether it is expressed implicitly or explicitly.

Our purpose in this document is to provide a complete formal semantics for the moccml language by using Plotkin's Structural Operational Semantics [START_REF] Gd Plotkin | A structural approach to operational semantics[END_REF]. This formalism provides a set of rules used to unambiguously specify the behavior or evolution of the elements composing the language. As a result, abstract mathematical reasoning and proof should be applied to the model defined in the language. Moreover, the rules of the formal semantics can be used for the implementation of an execution engine to provide simulation and exhaustive behavior exploration.

There exist different possibilities to write the formal semantics of models i.e.,axiomatic semantics, denotational semantics (sometimes referred as transformational semantics), or operational semantics. However, the operational semantics is closer to the definition of simulation engines, as it basically defines the step-by-step execution rules of a given language. The implementation of a simulator for moccml models is not the only aspect that operational semantics rules are used for. In fact, a simulator generally shows only the execution traces of one possible execution path. As such, the rules can also be used for the exhaustive exploration of all the possible execution paths.

In this document, we define an operational semantics for the moccml language. The sections in the document are structured in such a way that, we firstly provide a description of the grammar rules for the language syntax; then we provide the operational semantics rules. This document also presents two more parts to identify the elements of the moccml models that are relevant for simulation and to realize an exhaustive exploration on these elements.

Perimeter

This document is the version v1 of the D3.2.1 deliverable. The document addresses the operational semantics of the moccml language, the description of the elements that are relevant to specify the state of a moccml model as well as the rules that specify the evolution of this state. It also gives a first description of the way in which moccml models are used for exhaustive exploration.

Inria

Definitions, Acronyms and Abbreviations

• AS: Abstract Syntax.

• API: Application Programming Interface.

• Behavioral Semantics: see Execution semantics.

• CCSL: Clock-Constraint Specification Language.

• Domain Engineer: user of the Modeling Workbench.

• DSA: Domain-Specific Action.

• DSE: Domain-Specific Event.

• DSML: Domain-Specific (Modeling) Language.

• Dynamic Semantics: see Execution semantics.

• Eclipse Plugin: an Eclipse plugin is a Java project with associated metadata that can be bundled and deployed as a contribution to an Eclipse-based IDE.

• ED: Execution Data.

• Execution Semantics: Defines when and how elements of a language will produce a model behavior.

• GEMOC Studio: Eclipse-based studio integrating both a language workbench and the corresponding modeling workbenches.

• GUI: Graphical User Interface.

• Language Workbench: a language workbench offers the facilities for designing and implementing modeling languages.

• Language Designer: a language designer is the user of the language workbench.

• MoCC: Model of Concurrency and Communication.

• Model: model which contributes to the convent of a View.

• Modeling Workbench: a modeling workbench offers all the required facilities for editing and animating domain specific models according to a given modeling language.

• MSA: Model-Specific Action.

• MSE: Model-Specific Event.

• RTD: RunTime Data.

• Static semantics: Constraints on a model that cannot be expressed in the metamodel. For example, static semantics can be expressed as OCL invariants.

• TESL: Tagged Events Specification Language.

• xDSML: Executable Domain-Specific Modeling Language.

RR n°8584

Summary

In the GEMOC project, moccml is dedicated to define the MoC associated with the DSMLs. The purpose of this document is to define the operational semantics of the moccml language and also to define the first steps of an approach to provide an exhaustive exploration of the moccml models.

Chapter 2 presents the operational semantics of the moccml language. The chapter is divided in several sections that present the grammar rules of the language and the operational rules mainly defined using mathematical grounds and Plotkin [START_REF] Gd Plotkin | A structural approach to operational semantics[END_REF] rules. Chapter 3 presents the elements that are relevant to describe the evolution of a moccml model. Chapter 4 presents a draft of how exhaustive exploration is to be realized in a context using moccml models. Finally Chapter 5 presents the conclusion.

Inria

moccml semantics

The language is based on the definition of several RelationDefinition which provides clock constraints and the state based definitions. The operational semantics defined in the next sections define the semantics of these RelationDefinition.

First of all, the grammar rules are described using a BNF (Backus-Naur Form) notation. In this notation, we associate a meaning to the following symbols:

• ::= means is defined by

• A | B

means parallel composition of A and B ( if one of the term A or B is absent it means

A or B);

Operational semantics of the clock constraints

The operational semantics of the clock constraints is the operational semantics of the ccsl language [START_REF] André | Syntax and Semantics of the Clock Constraint Specification Language (CCSL)[END_REF].

Syntax of the moccml declarative operators

This section defines the syntax of the moccml declarative operators on a set of clocks C. With the primitive constructs provided by the kernel, new constructs can be derived and proposed in libraries. For the sake of conciseness, we use a symbolic notation for the kernel operators and constructs. There also exists a concrete textual syntax given in the deliverable D.2.2.1 for the state machine part and on the http://timesquare.inria.fr/index.php?slab=extendedccsl-grammar website for the declarative part.

To ease the writing of the semantics, we use a symbolic notation for the moccml declarative operators. The syntax in given in Tables 1 and3. The relation named "clock definition" is a simple clock relation which associates a clock with a clock expression. C includes all the clocks in the specification. Notice that in the declarative part of moccml, a clock relation applies to two clock references, themselves possibly defined by a clock expression.

| clock ∨ clock (sup) | clock ∧ clock (inf)

Semantics

We propose to give moccml an operational structural semantics that allows the effective construction of temporal evolutions. Note that we consider only clocks with a discrete set of instants.

moccml Declarative Model A moccml Declarative Model M = C, S consists of a finite set of discrete clocks C, constrained by a moccml C specification S. A moccml model is a set of constraints specified by a natural extension of ccsl [START_REF] André | Syntax and Semantics of the Clock Constraint Specification Language (CCSL)[END_REF]. Consequently, this document is a major update and extension of the [START_REF] André | Syntax and Semantics of the Clock Constraint Specification Language (CCSL)[END_REF] document.

mocc Specification A moccml system denotes a set of schedules. If empty, there is no solution, the specification is invalid. If there are many possible schedules, it leaves some freedom to make some choices depending on additional criteria. For instance, some may want to run everything as soon as possible (ASAP), others may want to optimize the usage of resources (e.g.,processors/memory/bandwidth). A schedule σ over set of clocks C is a possibly infinite sequence of ticking clocks. σ : N → 2 C .

Inria

Given a clock c, a step s ∈ N and a schedule σ, c ∈ σ(s) means that clock c ticks at step s for this particular schedule. f σ s denotes the set of ticking clock at step s in σ. The goal of the semantics rules is to be specify how to construct a specific schedule. To ease the reading, in the following rules we denote by F the set of fired clock at the current step for the schedule under construction.

Based on this, we can define the notion of History. Given a schedule σ, the History over a set of clocks C is a function H σ : C × N → N defined inductively as follows for all clocks c ∈ C:

H σ (c, 0) = 0 (1) ∀n ∈ N, c / ∈ σ(n) =⇒ H σ (c, n + 1) = H σ (c, n) (2) ∀n ∈ N, c ∈ σ(n) =⇒ H σ (c, n + 1) = H σ (c, n) + 1 (3)
In consequence, the history of a clock c at the current step during the construction of a schedule σ is H σ (c, now). Also, as a syntactic sugar construction, one can obtain the history in between two step s1 and s2 by using this construction: H σ (c, s1, s2), which is defined by

H σ (c, s2) -H σ (c, s1).
The semantics of a specification S expressed in moccml C is given as a Boolean expression on C , where C is a set of Boolean variables in bijection with C as defined later in equations 7 and 8. let π : C → C bijection, and

: kccl C → B C (4)
is defined by structural rewriting rules. For convenience, we denote π(c) by c, for all c in C. c = 1 means that c ∈ σ(now). More generally,

σ |= C, S if f (∀f ∈ σ : C → {0, 1}) C, S f -→⇔ S (f ) = 1 (5)
In Eq. 5, f is a valuation of C , S (f ) = 1 says that S evaluates to 1 for the valuation f . In the operational semantics rewriting rules, we refer to F as the subset of C in which only the clock that ticks at the current step are kept. The next two subsections detail structural transformations from moccml C to Boolean expressions on C (i.e.,B C ). In Boolean expressions, we use operators ⇒ (implication), = (equality), # (exclusion), and ite( , , ) (if . . . then . . . else . . . ) such that for any Boolean expression t 1 , t 2 , t 3 :

t 1 ⇒ t 2 ⇔ ¬t 1 ∨ t 2 t 1 = t 2 ⇔ (t 1 ∧ t 2 ) ∨ (¬t 1 ∧ ¬t 2 ) t 1 # t 2 ⇔ ¬t 1 ∨ ¬t 2 ite(t 1 , t 2 , t 3 ) ⇔ (t 1 ∧ t 2 ) ∨ (¬t 1 ∧ t 3 )
A first rule is given right now. This rule expresses the composition of clock relations: the parallel composition of clock relations is the conjunction of the associated Boolean expressions.

CR 1 | CR 2 = CR 1 ∧ CR 2 ( paral ) (6) RR n°8584
Clocks A clock c is a possibly infinite ordered set of instant I c . I c possibly contains two specific instants, its birth denoted c † and its death denoted c † . The birth always precedes the first instant of its clock and its death is its last instant (possibly synchronous with another instant).

c † ∈ I c ∧ c † ∈ I c c = c ( clock1 ) (7) c † ∈ I c ∨ c † ∈ I c c = ¬c ( clock2 ) (8)

Clock relations

for some of the following rules, we can distinguish two different natures for the semantics rules. The first kind defines the projection of the constraint to their Boolean representation. The second kind defines the possible propagation of birth and death among the parameter of the constraints.

Conditional clock relation A Clock relation can be defined conditionally to some Boolean β. When β is false, CR if β is true, whatever the clock relation. Else, we have to compute the Boolean expression associated with the clock relation.

CR if β = (β ⇒ CR ) ( rcond ) (9)
History-independent clock relations Sub-clocking c 1 is a subclock of c 2 (or c 2 is a superclock of c 1 ) means that each instant of c 1 must be coincident with an instant of c 2 . In logical words this says that c 1 ticks only if c 2 ticks, hence the logical implication.

c 1 ⊂ c 2 = (c 1 ⇒ c 2 ) ( subclock ) (10) c † 2 ⇒ c † 1 ( subclock death propagation ) (11)
Recall that c = c .

Clock exclusion Two clocks c 1 and c 2 can be declared exclusive, that is, none of their instants are coincident, or equivalently, it is forbidden that both c 1 and c 2 tick at a configuration. This is expressed by the Boolean expression

c 1 # c 2 equivalent to ¬(c 1 ∧ c 2 ) and ¬c 1 ∨ ¬c 2 . c 1 # c 2 = (c 1 # c 2 ) ( excl ) (12)
Clock equality This is a special case of double subclocking, there is a bijection between the sets of instants of the two clocks. The Boolean expression states that c 1 ticks if and only if c 2 ticks and conversely.

c 1 = c 2 = (c 1 = c 2 ) ( coinc ) (13) Inria c † 2 ⇔ c † 1 ( coinc death propagation ) (14)
Clock definition The left-hand side clock ticks whenever the right-hand side clock expression ticks; also the death of one of them is propagated to the other one.

c CE = (c = CE ) ( clockDefinition ) (15) c † ⇔ CE † ( clockDefinition death propagation ) (16)
History-dependent clock relations The next two clock relations depend on the history of the concerned clocks. More precisely they depend on the difference of their own history. Let δ H(c 1 , now) -H(c 2 , now).

Clock precedence c 1 ≺ c 2 is read "c 1 precedes c 2 ". This means that for any step s in a schedule that satisfies the moccml specification, H(c 1 , s) ≥ H(c 2 , s). This formulation is less intuitive than the following: for any natural number k, the k th instant of c 1 strictly precedes the k th instant of c 2 . This precedence between instants explains that this relation is also read as "c 1 is faster than c 2 ". According to this definition, c 1 , which is the faster of the two clocks, is never constrained. As for c 2 , it is constrained only when its index becomes equal to the index of c 1 .

Under such a circonstance, c 2 can not tick.

β (δ = 0) c 1 ≺ c 2 = (β ⇒ ¬c 2 ) ( precede ) (17)
Another consequence of this rule is that the following invariant property holds:

Invariant: δ 0 c † 1 ∈ I c1 ∧ c † 2 ∈ I c2 ∧ δ = 0 c † 1 ⇒ c † 2 ( precede death propagation ) (18)
Clock causality The cause relation is similar to the previous one. The unique difference is in the possibility for c 2 to tick when δ = 0, provided that c 1 also ticks. Hence the Boolean expression involves two implications.

β (δ = 0) c 1 c 2 = β ⇒ (c 2 ⇒ c 1 ) ( prec ) (19)
The invariant property on δ still holds:

Invariant: δ 0 c † 1 ∈ I c1 ∧ c † 2 ∈ I c2 ∧ δ = 0 c † 1 ⇒ c † 2 ( cause death propagation ) (20)
RR n°8584

Clock expressions

During the construction of a schedule, clock expressions may change. So, we introduce conditional rewriting rules for clock expressions. A rewriting is expressed as CE → CE ′ where CE ′ replaces CE after a firing which meets the condition. Of course, the constraint parameters can also be rewritten.

A clock expression has an associated implicit clock In the rules below, c stands for the clock associated with the current clock expression.

For all the following semantic rules; there is no death propagation since it can always be added by using additional relations.

Conditional clock expression A conditional clock expression defines a clock that behaves either as a clock c 1 or as another clock c 2 according to the value taken by the Boolean β.

β ? c 1 : c 2 = ite(β, c 1 , c 2 ) ( econd ) (21)
Terminating clock expressions Terminating clock expressions define finite clocks (i.e.,clocks that eventually die). These clock expressions are used to build more complex clock expressions, especially through the clock concatenation.

Wait The wait clock expression c1ˆn ticks in coincidence with the next n th strictly future tick of c 1 , and then dies.

β (n = 1) c 1 ˆn = (β ∧ c 1 ) (moccml await ) (22)
c 1 ∈ F c 1 ˆ1 → I c = I c + c † ( RWawait1 ) (23)
c 1 ∈ F n > 1 c 1 ˆn → c 1 ˆ(n -1) ( RWawait2 ) (24)
Strict sampling Sampling clock expressions involve two clocks. The first is considered as a trigger and the second as a time base. The sampling expression ticks in coincidence with the tick of the base clock immediately following a tick of the trigger clock, and then dies. There exist two versions of the sampling: either the strict one (the coincident tick of the base clock is strictly after the trigger tick) or the non-strict one (the coincident tick of the base clock may be coincident with the trigger tick when this one is coincident with a base clock tick).

c 1 c 2 = c ( ssampl ) (25) c 1 ∈ F c 1 c 2 → c 2 ˆ1 ( RWssampl ) (26)
Non strict sampling

Inria c 1 ↓ c 2 = (c 1 ∧ c 2 ) ( sampl ) (27) c 1 ∈ F c 2 ∈ F c 1 ↓ c 2 → I c = I c + c † ( RWsampl1 ) (28) c 1 ∈ F c 2 ∈ F c 1 ↓ c 2 → c 2 ˆ1 ( RWsampl2 ) (29)
Preemption The premption expression c 1 c 2 behaves like c 1 while c 2 does not tick. When c 2 ticks, the expression dies.

c 1 c 2 = (c 1 ∧ ¬c 2 ) ( upto ) (30)
c 2 ∈ F c 1 c 2 → I c = I c + c † ( RWupto ) (31)
Non-terminating index-independent clock expressions These clock expressions contrast with the terminating ones: they don't have explicit death. Among them, many are historyindependent.

Clock concatenation

The concatenation clock expression c 1 • c 2 behaves like c 1 up to the death of c 1 . When c 1 dies, the expression behaves like c 2 . The concatenation may induce recursive definitions.

c 1 • c 2 = c 1 ( concat ) (32) c = c 2 c † 1 ∈ I c1 c 1 • c 2 → c 2 ( RWconcat ) (33) c † 1 ∈ I c1 c 1 • c → I c1 = I c1 -c 1 † ( RWrecur ) (34)
Clock union The union clock expression c 1 + c 2 ticks whenever c 1 or c 2 ticks.

c 1 + c 2 = (c 1 ∨ c 2 ) ( union ) (35)
Clock intersection The intersection clock expression c 1 * c 2 ticks whenever both c 1 and c 2 tick.

c 1 * c 2 = (c 1 ∧ c 2 ) ( inter ) (36)
Clock delay The delay clock expression c 1 (ns) c 2 is a rather complex expression involving two clocks (c 1 , c 2 ) and a sequence of natural numbers (ns). c 1 is a trigger, c 2 a base clock. At each tick of c 1 the head of ns is dequeued and encoded in a binary word bw associated with the expression. This binary word is a kind of "diary" that contains the future rendez-vous with c 2 ticks. For instance, when c 1 ticks and the head of ns is 5, then the expression is expected to tick in coincidence with the next 5 th tick of c 2 . Note that rendez-vous are not necessarily taken in a monotonic increasing order.

β (bw = 1.w) c 1 (ns) c 2 = (β ∧ c 2 ) ( defer ) (37)
c 1 ∈ F c 2 ∈ F b ∈ {0, 1} c 1 (ns) c 2 , b.w → c 1 (ns) c 2 , w ( RWdefer1 )
(38)

c 1 ∈ F c 2 ∈ F h ∈ N ⋆ c 1 (h.s) c 2 , w → c 1 (s) c 2 , w + (0 h-1 .1) ( RWdefer2 )
(39)

c 1 ∈ F c 2 ∈ F b ∈ {0, 1} h ∈ N ⋆ c 1 (h.s) c 2 , b.w → c 1 (s) c 2 , w + (0 h-1 .1) ( RWdefer3 ) (40)
Non-terminating index-dependent clock expressions The last two clock expressions depend on the clock history H, or more precisely on the difference of two clocks histories.

The fastest of slower clocks The sup clock expression c 1 ∨ c 2 defines a clock that is slower than both c 1 and c 2 and whose k th tick is coincident with the later of the k th tick of c 1 and c 2 .

β 1 (H(c 1 ) = H(c)) β 2 (H(c 2 ) = H(c)) c 1 ∨ c 2 = (β 1 ⇒ c 1 ) ∧ (β 2 ⇒ c 2 ) ( sup ) (41) Invariant: H(c) = min{H(c 1 ), H(c 2 )} and β 1 ∨ β 2 = 1
The slowest of faster clocks This expression is the dual of the previous one. The inf clock expression c 1 ∧ c 2 defines a clock that is faster than both c 1 and c 2 and whose k th tick is coincident with the earlier of the k th tick of c 1 and c 2 .

β 1 (H(c) = H(c 1 )) β 2 (H(c) = H(c 2 )) c 1 ∧ c 2 = (β 1 ∧ c 1 ) ∨ (β 2 ∧ c 2 ) ( inf ) (42) Invariant: H(c) = max{H(c 1 ), H(c 2 )} and β 1 ∨ β 2 = 1 Inria 2.

State machine operational semantics

The moccml language allows the definition of libraries of constraints on clocks with equational and state based support. The libraries are defined throught RelationDefinition and StateBase-dRelationDefinition. As such, we assume that the elements defined in the StateRelationBas-edLibrary are equivalent to clock relations. For instance, the StateBasedRelationDefinition is a primitive for the description of a new relation between clocks. The description of the semantics is divided in two parts: The first part gives a description of the grammar rules highlighting the syntax of the moccml; the second part defines the dynamic evolution of state-based clock relations defined with moccml.

Syntax Notation

For the sack of simplicity, we will consider that a CR f sm is defined between several clocks, sometimes using additional formal parameters that are not clocks, eg Integer, Real or Sequence. A CR f sm can also be defined as a set of clocks assiociated with ( ) an CE (Clock Definition). Table 4 shows the rules corresponding to these considerations. The impact of contraints on behaviors is dependent of the evaluation of guards and triggers (presence, absence, returned evalutation value). Accordingly, the grammar rules of the StateBasedRelationDefinitions are presented in the Tables 5 and6 that declare the primitives composing the StateBasedRelationDefinition.

::= Q → (G)? / (A)? → Q (transition)
Naturally speaking, a StateBasedRelationDefinition is composed of declaration blocks DB, of a set of states Q and set of transitions T . The declaration blocks is made up with linear expressions LE on Integers, boolean expressions on Integers BEI, classical boolean expressions BE or concrete entities C E , i.e.,clock or int. The set of states is made up with an initial state

Q 0 ∈ Q, several intermediate states (Q I ∈ Q ∧ Q 0 ∈ Q I ∧ Q T ∩ Q I = ∅) and possibly several finale (or terminal) states (Q T ∈ Q ∧ Q 0 ∈ Q T ∧ Q T ∩ Q I = ∅).
States can have input or ouput transitions except for the finale states that do not define output transitions. A transition goes from a state to another and can possibly define a guard and an action. A guard contains from 0 to 3 parts: an optional boolean guard, a first set of clock, which represent the clock that need to tick for the transition to be triggered and a second set of clock, which represent the clock that need to not tick for the transition to be triggered. Finally, there are three different kind of actions (i.e.,IntegerAssignment, IntegerAssignmentBlock or FinishClock ).

State based relation operational Semantics

As described in Section 2.1.2, a moccml system is a tuple C, S , H, where C is the set of Clock, S is the specification of clock constraints and H is a given history. The semantics r f sm op of r f sm op is given as a Boolean expression on C , where C is a set of Boolean variables in bijection with C which is obtained according to a given history, the current state cr st of r f sm op , where cr st ∈ Q; the evaluation of boolean guards and of the triggers on transitions of a StateBasedRelationDefinition. The rewriting rules depends on the fired transition and their actions.

If we consider the Figure 1 illustrating an example of state-transition automata. We define cr st as the current state of the state machine where cr st ∈ Q. For a given cr st (crt) which is not the initial state, there is possibly one to many possible input transitions for a state (e.g.,t0,t1,t2) and zero to many output transitions (e.g.,t2,t3,t4,t5). We will not focus on the input transitions because only the output transitions of cr st are used in the construction of r f sm op . Let T o being the set of output transitions of the current state.

Note: in the following we do not detail the semantics of boolean expressions (which is a classical boolean algebra and integer comparison). We use the same facilities for expressions on integers.

State Machine

C T rue ⊂ F ∧ ∀c ∈ C F alse , c ∈ F ∧ t.source = cr st cr st = t.target ∧ A ( transition rewriting ) (45)
The semantics of a transition t is given by the coupling of: the semantics of the guard associated to it and the rule reifying the transition rewriting function between a source state and a target state. The transition rewriting function depends on a couple of premises. Considering t.source as the cr st , if C T rue ∈ F and C F alse / ∈ F , then with the evalution of guard the next cr st is t.target and an action is potentially performed.

Guard guard = BE < BE, C T rue , C F alse > = guard ∧ ( c∈C T rue c) ∧ ( c∈C F alse ¬c) ( guard ) (46)
For a given guard and its boolean expression. Depending on the value of the boolean expression, the c ∈ C T rue tick, when the c ∈ C F alse does not tick. When the c ∈ C F alse ticks or the guard evaluation is false, then the transition is not operated. finish action

RR n°8584 kill(c) = (I c = I c + c † ) ( finish action ) (47)
A finish clock action (kill(c)) implies the death of the clock c.

3 Runtime State definition of a moccml state machine A moccml state-based model has a state which evolves all along a schedule. This state relies on the definition of the history of the set of clocks. Naturally speaking, the "runtime state" of a state machine contains the current state of an instance of the state machine and the values of each of its local variables.

Configuration definition

The history of a moccml Declarative Model M = C, S for a specific schedule σ has been defined as

H σ : C × N → N (see section 2.1.2).
The definition of a moccml state-based model history extends the previous definition with two more parameters, i.e.,: the current states of each state machines and the values of each local variable.

We expand the history H σ into three combined functions and formalize it as follows:

H σ ::=      H c σ : C × N → N relation (1) H q σ : 2 Q × N → 2 crst relation (2) H CE σ : 2 CE × N → N relation (3) (48)
The first relation is similar to the one defined in Section 2.1.2, it associates to a clock in C and a step number in σ the number of tick of the clock at this step. From now, the history H σ from Section 2.1.2 is replaced with H c σ . In the second relation, for a given set of set of state (i.e.,the states from all state machines ∈ S) and a step number in σ, H q σ provides the set of current state of each state machine. The third relation says that for a given set of concrete entities (the union of the ones in the declaration blocks of each state machine ∈ S and a given step number in σ), H CE σ provides the set of all the concrete entities values.

At each step in the history, the clocks ∈ S, the state machine ∈ S and the concrete entities in the declaration blocks of the state machines ∈ S are considered to determine the current history.

Towards an exhaustive exploration

The goal of this chapter is to define the approach which provides the capacity to explore the behavior of the moccml model associated with the dsml model. This functionality provides the exploration of all the possible behaviors of the mocc associated with the dsml model.

During the Gemoc project, the simulation functionality is the main focus to obtain a trace of the model execution based on the language workbench tooling. Regarding the exploration, the simulation trace represents a subset of the exploration and so a subset of the behaviors of the mocc. The exploration is possible in the scope of the mapping definition between the mocc and the dsml. The definition of this mapping must take into account the capacity of the exploration and the constraints with it.

Inria

A moccml model exploration is necessarily based on a configuration definition and also a definition of an abstraction of the behavior of the DSE events and DSA actions from the explorer point of view. This abstraction definition must be defined to close the explored behavior.

The definitions of this chapter are the first attempt to define the methodology to explore the behaviors of the moccml model.

Configuration definition

A moccml state-based model configuration relies on the history of the set of clocks, the set of the current states of a StateBasedRelationDefinition and the values of the set of local variables.

In our case, these configurations are defined as the configurations of a Labeled Transition System where the states encode all the current states of the state machines and the current values of the RTD variables. The transitions between states are labeled by the events of the fired events in the state machine behaviors of the given StateBasedRelationDefinition .

In this context, the methodology consists of a selection of the events mapped to clocks and the selected variables that are defined as RTD. According to the definition of the section 3, the possible type of the variables is Integer.

The selection of the number of variables and clocks is very important to obtain an explorable statespace. So one of the methodology key features can be to provide guidelines to define amenable to exhaustive exploration.

dsml abstraction

The mapping between dsml and moccml is made at the ecl specification level. In this specification, we define events associated with the actions of the DSA and also events associated with the DSE events. On these event bindings we apply the moccml relations of the MoC Library to schedule the events. To make an exhaustive exploration of the finite state space of a system using such scheduling constraints, the idea is to abstract the DSA/DSE behaviors of the dsml in the form of state machines that will be synchronized with the moccml state-based relations instantiated on dsml models.

Figure 2 illustrates the elements that are taken into account to provide exhaustive exploration and simulation. The first two lines of the figure show the ecl mapping ( 5 ○) definition which takes as inputs DSA ( 1 ○), DSE ( 2 ○) and the moccml relations ( 3 ○). The ecl mapping is applied to the dsml models ( 4 ○) to unfold all the relationships defined in the ecl mapping for this dsml instance. The resulting model is the dsml +moccml instance ( 7 ○). The state machines ( 6 ○) corresponding to the behavior of the DSA/DSE are also generated from the ecl mapping ( 5 ○). To stay within a purely state-based description style, these abstractions related to DSA/DSE behaviors are made in the form of StateBasedRelationDefinition.

The previous unfolding step, coupled to abstract state-based behaviors (DSA/DSE), allows building the finite state space that will be used for exhaustive exploration (eg OBP) or simulation (e.g.,TimeSquare).

Conclusion

This document presents the operational semantics of the moccml language which was defined to create mocc models associated with any dsml.

This semantics is an extension of the ccsl language definition based on equational relations completed by state based relations. The formal semantics of the moccml language allows for a composition of the two kinds of relations and is amenable to simulation, i.e.,the construction of schedules , which satisfy the models. The semantics uses the notion of history, which is used as a basis to define the notion of "runtime state" itself under study to extend the tooling associated with moccml towards an exhaustive exploration of the moccml models.

The tooling (moccml editor, TimeSquare, ecl language and the OBP explorer) around the moccml language must be aligned, or take into account, the definitions of this document.

References

  CR f sm ::= (simple state-based clock relation) (clock) * r f sm op (clock) * | (clock) * CE (clock definition) r f sm op is a special type of clock relation operator that defines constraints between clocks using finite state machine (FSM). A clock is a formal parameter of the clock relation, and is defined as a discrete clock type. The set of all clocks is defined by C. The formal parameters that are different from clocks (eg Integer or Real ) are used for the evaluation of guards or for actions within the transitions.

  CE ::= clock | int (set of concrete entities) LE ::= int LEop int (linear expression) LEop ::= + | -(linear expression operator) BEI ::= int BEIop int (boolean expression on integers) BEIop ::= = | < | > (operators on integer boolean expressions) BE ::= (boolean expression) BEI | BE or BE | BE and BE | not BE G ::= (BE)? (CT rue)? (C F alse )? (guard) CT rue ::= (clock) * (true trigger) C F alse ::= (clock) * (false trigger) A ::= (Aassign | A block | A f inish )* (action) AAssign ::= int = LE (integer assignment action) A bloc ::= (Aassign)+ (integer assignment block action) A f inish ::= kill(clock) (finish clock action)

Figure 1 :

 1 Figure 1: Partial automata Sample: crt = cr st

Figure 2 :

 2 Figure 2: Mapping architecture overview

Table 1 : moccml constraints and relations

 1

	CC	::=			(clock constraint)
			CC | CR		(parallel composition)
		|	CR
		|	CR if bool	(conditional constraint)
	CR	::=			(clock relation)
			clock r op clock
		|	clock	CE	(clock definition)
					Continued on next page
	RR n°8584

Table 2 :

 2 Relation operators

	r op	::=		(relation operator)
			⊂	(subclocking)
		|	#	(exclusion)
		|	=	(coincidence)
		|	≺	(s_precedence)
		|		(precedence)

Table 3 :

 3 moccml clock expressions

	CE	::=			(clock expression)
			bool ? clock : clock		(conditional expression)
		|	clock		(clock reference)
		|	clockˆnatural		(wait)
		|	clock clock		(s_sample)
		|	clock ↓ clock		(sample)
		|	clock clock		(upto)
		|	clock • clock		(concat)
		|	clock + clock		(union)
		|	clock * clock		(inter)
		|	clock(naturalSequence)	clock	(defer)

Table 4 :

 4 State-Based Relation grammar Notation

Table 5 :

 5 Grammar rules for moccml StateBasedRelationDefinition-Part 1

	r f sm op	::= (DB)? (Q | T ) *	(fsm-based clock relation operator)
	DB	::= (LE | BEI | BE | CE) *	(declaration block)
	Q	::= Q0 QI QT	(state set)
	Q0	::= state	(initial state)
	QI	::= (state)*	(intermediate state set)
	QT	::= (state)*	(terminal state set)
	T

Table 6 :

 6 Grammar rules for moccml StateBasedRelationDefinition-Part 2

RR n°8584

Inria

route des Lucioles -BP 93 06902 Sophia Antipolis Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

This document was partially founded by the ANR GEMOC project ANR-12-INSE-0011 7271