Vlad Rusu
email: vlad.rusu@inria.fr

Dorel Lucanu

A K-Based Formal Framework for Domain-Specific Modelling Languages

We propose a formal approach for the definition of domainspecific modelling languages (dsmls). The approach uses basic Model-Driven Engineering artifacts for defining a dsml's syntax (using metamodels) and its operational semantics (using model transformations). We give formal meanings to these artifacts by mapping them to the K semantic framework. Since the K definitions are executable, one obtains an execution engine for dsmls and gains acces to K's formal analysis tools. We illustrate the approach on xspem, a language for describing the execution of tasks constrained by time, precedence, and resources.

Introduction

Domain-Specific Modelling Languages (dsmls) are languages dedicated to modelling in specific application areas. Recently, the design of dsmls has become widely accessible to engineers trained in the basics of Model-Driven Engineering (mde): one designs a metamodel for the language's abstract syntax; then, the language's operational semantics is expressed using model transformations over the metamodel. The democratisation of dsml design catalysed by mde is likely to give birth to numerous languages, and one can also reasonably expect that there shall be numerous errors in those languages. Indeed, getting a language right (especially its operational semantics) is hard, regardless of whether the language is defined in the modern mde framework or in more traditional ones.

Formal methods can help detect or avoid errors in dsml definitions. However, the history of formal methods offers many examples of valorous methods that could not be transferred outside a circle of specialised users, because software engineers do not have the time or the background required for learning them. The lesson learned from these failures is that, in order to be accepted by software engineers, formal approaches have to operate with notions familiar to them.

We propose here such an approach, which formalises the basic mde ingredients used in dsml definitions. From the point of view of a user, the approach is a black box (Figure 1): users can define their dsmls using familiar mde ingredients (metamodels for syntax, ocl [START_REF]The object constraint language[END_REF] constraints for static semantics, model transformations for operational semantics). These inputs are are mapped to K [START_REF] Roşu | An overview of the K semantic framework[END_REF] code.

Here Be Rascal and K dsml's informal definition in model-driven engineering dsml's static & operational semantics in K (formal & executable) Fig. 1. Our approach, from the point of vue of a user defining a dsml.

In this way, users benefit from K's execution engine and formal analysis tools for free -without having to write code unfamiliar to them -which allows them to experiment and to formally analyse their languages in a transparent way.

We illustrate the approach on xspem [START_REF] Bendraou | Definition of an executable spem 2.0[END_REF], a dsml based on the omg standard [START_REF]Software & systems process engineering metamodel specification (spem[END_REF] for describing the execution of activities constrained by time, resources, and precedence relations. We show how users can automatically: check model-tometamodel conformance (including ocl constraints); execute a dsml's semantics; and model check for reachability properties over the dsml's executions.

Contributions Our main contributions is providing a formal semantics to the mde notions employed in dsml definitions, using the K semantical framework:

metamodels, together with well-formedness ocl constraints, and models; model transformations for operational semantics. We have designed for this a language called kmrl (K-based Model-Rewrite Language) by building on basic mde notions. kmrl is composed of model-rewrite rules, where each rule consists of a model pattern similar to mde-models, an optional condition written in ocl, and an optional piece of imperative code extending ocl. kmrl should therefore look and feel familiar to our target users: software engineers familiar with such basic mde notions as model and ocl constraints.

Note that in our approach, the user does not define the semantics of her/his dsml directly in K (we provide users with automated means for that instead). We do not advocate direct definitions in K, since K is unlikely to be accepted by users, and we have stated that the main motivation for this work is to gain user acceptance (and, ultimately, to further the cause of formal methods in practice).

Organisation Section 2 provides preliminaries: it describes the K semantical framework and illustrates the mde-based definition of the xspem domain-specific modelling language. In Section 3 we present our approach and illustrate it on xspem. Section 4 concludes and presents related and future work.

Preliminaries

2.1 The K Framework K [START_REF] Roşu | An overview of the K semantic framework[END_REF] is a framework mainly intended for defining and analysing semantics of programming languages 3 . The main features of K include:

executability: the definitions are directly executable in order to be experimented with and analysed; unique definition: there is only one definition for a language, and several analysis tools that are sound with respect to this definition; program logic: the framework serves as a program logic with which the programs can be verified and analysed (see, e.g., [START_REF] Roşu | Matching logic: An alternative to Hoare/Floyd logic[END_REF]).

A K definition has three main ingredients: a configuration, which is a structure of nested cells abstracting the state structure of the machine on which the programs are executed; computations, which are sequences of tasks derived from an annotated syntax; and K rules, which describe computation steps using minimal information (only what is needed for matching and rewriting). These concepts are illustrated in Section 3. Then, the K execution engine can be used for executing the definition, and its model checker, for checking reachability properties.

Defining a DSML using MDE: xSPEM

We illustrate our approach on a dsml called xspem [START_REF] Bendraou | Definition of an executable spem 2.0[END_REF], which is an executable version of the spem language standard [START_REF]Software & systems process engineering metamodel specification (spem[END_REF]. The language describes the execution of activities constrained by time, resources, and precedence relations. We first describe the syntax and static semantics of (a simplified version of) xspem by showing its metamodel as well as a sample model. Then we describe the language's operational semantics using a mixture of graphical and textual notations. These notations will become formal when we represent them in K.

In the metamodel of Figure 2 (top), activity is the class of entities being executed. The tmin and tmax attributes of the activity class denote the minimum and maximum expected duration of activities. The aS attribute takes its values in the activityState enumeration: notStarted, inProgress, or finished ; and the tS attribute takes its values in the timeState eumeration: undefined, tooEarly, ok, or tooLate. An activity may also have resources, which are reserved by the activity (and become unavailable to others) while the activity is running. In addition to the availability of resources (resource class) the execution of activities is also governed by explicit ordering constraints (workSequence class). Each activity also has exactly one workSequence instance, as indicated by the ocl invariant associated to the metamodel. The workSequence class has references to four possibly empty sets of activities, namely, the activities that must be started for the current activity to start (startedToStart reference); finished for the current activity to start (finishedToStart reference); started for the current activity to finish (startedToFinish reference); finished for the current activity to finish (finishedToFinish reference). Time is measured by a clock, encoded by the time attribute of the process class. Activities inherit from processes (inheritance is denoted in class diagram by an open arrrow). Hence, activities also have the time and activities features.

In the model depicted at the bottom Figure 2, the activities a and b are linked by a workSequence via the reference finishedToStart, meaning that b is allowed to start only when a is finished; and a has the (available) resource r.

We now give the operational semantics of xspem using a semi-formal notation mixing graphical and textual rules. The notation is isomorphic to the (textual) kmrl language that we shall formalise in Section 3.5. The first rule is shown in Figure 3. It expresses the fact that processes "make time pass": the time attribute is increased by one. This is expressed by a local rewrite rule (a concept inspired from K): time = (T ⇒ T + 1 ), within a process X. Here, X and T are variables (of type process, respectively, integer) to be matched with correspondingly typed constants in a model; when this happens, the model is rewritten, just like in usual rewrite systems. For example, the execution of this rule on the model shown at the bottom of Figure 2 would produce the same model except that p.time = 1. The next rule (Figure 4) expresses the starting of an activity. When an activity Y is started, the value of its aS attribute is rewritten from notStarted to inProgress, and the activity Y memorises in its time attribute the value of the homonymous attribute of the process, say X, which owns the activity. This is expressed by the local rewrite rule time = ( ⇒ T ), which says that the time attribute of X is rewritten, from whatever value it had, to T ; where "whatever" is denoted by an underscore, and T equals the value of X .time. Moreover, the activity Y may only be started if the (optional) when condition holds; and, finally, some additional imperative code, in the (optional) then clause, is executed.

Here, the when clause says that the activities that have to be started (resp. finished) for the current activity Y to start are indeed in the expected states, and that all the resources of Y are available. The additional code in the then clause is here an imperative for loop, which is in charge of assigning all the activity's resources available attributes to false. In general, the additional code can include assignments, loops, and conditionals, and can declare local variables for storing intermediate values. The practical utility of the imperative code can be illustrated on the current example: when an activity is started, it needs to make all its resources un-available to other activities; but this cannot be expressed in a graphical rewrite pattern, because an activity may have any number of resources; whereas a graphical pattern "draws" a fixed number of model elements.

The semantics of xspem includes one other rule in addition to the two ones shown above. The third rule is in charge of finishing activities. It is shown in Figure 5. The main difference with the rule for starting an activity lies in the more complex imperative code, which is here used for updating the tS attribute of the activity Y being terminated, to tooEarly, ok, or tooLate, depending on whether its execution time is in [0,tmin), [tmin,tmax ) or [tmax ,∞), respectively. This is achieved using two nested if-then-else-endif conditionals. In order to avoid recomputing the execution time T -T , we store it in the local variable x.

Hence, we have a flexible and expressive declarative/imperative language for describing operational semantics of dsmls. In order to make it formal and executable we map it (together with languages for expressing metamodels and models for dsmls) to the K framework, which we now briefly introduce.

A K-Based Formal Framework for DSMLs

A General Overview

In this section we show how mde concepts used in defining dsmls can be mapped to K. The mapping is implemented in the Rascal metaprogramming language [START_REF] Klint | Rascal: A domain specific language for source code analysis and manipulation[END_REF].

A dataflow diagram of our approach is shown in Figure 6. It consists of: a Rascal program, which takes as input the ingredients of a dsml definition (metamodel, ocl constraints, models, kmrl rules) in a certain textual format, and produces the corresponding K code; a K program, which together with the output produced by Rascal, and with additional K code defining the semantics of ocl and kmrl, constitute the formal static semantics and formal operational semantics for the dsml; the K semantics of the dsml is then compiled by the K tool in order to get an executable semantics, which is used for simulation (experimentation) and analysis.

Note that from the point of view of dsml designers, the outmost box is a black box: they do not need to know what is inside, but only need to provide the mde artefacts for the definition of their dsml in a textual format; then, the static and operational semantics of the dsml is automatically generated for them. We now describe the framework in detail by "scanning" the diagram in Figure 6 from left to right, and illustrate it on the xspem language from Section 2.2.

Metamodels and OCL constraints

We show in Figure 7 the textual syntax for the xspem metamodel from Figure 2. In order to generate input for K, the metamodel in textual syntax is processed by a Rascal program. This includes parsing and some syntactical transformations, such as the replacement of multiplicity constraints and bidirectionality constraints by equivalent ocl invariants. For example, the [1-1] multiplicity of the workSequences reference is replaced by the equivalent ocl invariant allInstances(activity)→forAll(x:activity|x.workSequences.size() = 1).

The metamodel is thus stripped of its multiplicity and bidirectionality constraints and the result is translated to a set of K function declarations together with rules to evaluate them. The functions encode all the (stripped) metamodel's information: for each enumeration, its set of values, and for each class, its children classes, its attributes with their types, and its references with their types. They are used for checking the syntactical correctness of models with respect to the given metamodel. This is discussed in more detail in Section 3.3.

Well-formedness OCL constraints In addition to the implicit constraints induced by multiplicities and bidirectionality of references, a metamodel may include other ocl constraints, which enforce well-formedness requirements that models conforming to the metamodel must satisfy. For example, we shall require that in any well-formed xspem model there is exactly one "proper" process:

(allInstances(process) \ allInstances(activity)).size() = 1.

Models

In dsml terminology, models can be seen as "dsml programs", by analogy with the programs of usual programming languages. In this section we show the syntax of models required as input by our Rascal module in charge of processing models, and the representation of the models as K configurations generated by the module in question. In the next section we outline of the K semantics for ocl, and show how model-to-metamodel conformance checking is done in K.

We also use textual language for the model description. The essential information about a model consists of the name of the metamodel it must conform to and a collection of objects (class instances). Each object is described by its name, the class it belongs to, and the values of its attributes and references.

In Figure 8 we give the equivalent textual syntax for a fragment of the xspem model example given in Figure 2. Using this input together with the information obtained from a metamodel and ocl constraints, a Rascal module generates a K configuration described as follows.

K Configuration for DSMLs K configurations are structures consisting of nested cells. The generic K configuration for dsmls is graphically represented in Figure 9. The configuration includes: a cell model for models (described later in this section); a cell oclConstraint containing ocl constraints to be checked on the model; a cell k containing computation tasks to be performed on the model (conformance checking, model execution, model checking, . . . ); and a cell result for storing the results of the computation tasks. Initially, the cells are empty (as denoted by periods and dashes within them, depending on their type). They are filled by Rascal modules: the model cell is filled by the module in charge of models, and cell oclConstraint cell is filled by the module in charge of ocl constraints of the metamodel to which the model is supposed to conform. The structure of the cell model is similar to that of the textual language we use for model description. It consists of a set of instance cells, each of which contains the instance's name, its class, and its attribute/reference values.

K Semantics of OCL

We have defined in K a substantial fragment of ocl based on the standard [START_REF]The object constraint language[END_REF]. Due to limited space, a complete description will be given in a separate paper.

The elementary types in our definition of ocl are integer, string, and Boolean with the usual elementary operations on them. We also allows for collection types, built using navigation through attributes/references, iterators (select, collect), quantifiers (forAll, exists), as well as the usual set operations. The allInstances() query returns all the instances of a given class. This provides us with a rich language for constraints, which we may enrich in the future.

Here is, for instance, the K rule giving semantics to the query allInstances():

allInstances(Cls)
val(collectAllInstanceNames(Cls , children(Cls) , M)) The rule says that, in order to compute all the instances of a given class Cls in a model M, a helper function collectAllInstanceNames() must be called, with three parameters: the class Cls, its children children(Cls), and the model M.

••• k M model -- oclConstraints • k • result -- instName --
The fraction line denotes a local rewrite, here, at the the head of the computation cell k . The numerator is what is usually written in the left-hand side of rewrite rules, and the denominator is the equivalent of the right-hand side. A K rule may have several local rewrites in various configuration cells, and it can use other cells just for providing context of the rewrite. For example, in the above rule, the cell model provides the model M. The operator children() is a part of the K description of the metamodel, and the function collectAllInstanceNames() traverses the instance cells of M and collects their names. The semantics of the later function is given by a set of similar K rules. Finally, the val operator wraps the result in order for K to interpret it as a fully eveluated ocl value (in our case, a collection of instance names).

As another axample, we give the K semantical rules for the forAll operation in order to illustrate some interesting features of K. Syntactically, the operation is written Col->forAll(Id | Exp), and its meaning is that it is true if and only if the third argument Exp evaluates to true on each element (denoted by the second argument Id) of the first argument Col. Its K semantical rules are

val( • )->forAll(Var | Exp) true ••• k (1)
val(Hd, Tl)->forAll(Var | Exp)

if Exp(Hd/Var) then val(Tl)->forAll(Var|Exp) else false

••• k (2)
The first rule describes the base case, when the first argument is an empty collection. The second rule describes the inductive step: when the first argument is a nonempty collection of the form val(Hd, Tl), the result depends on the value of the expression Exp on the element Hd. This value is computed by applying the K visitor pattern [START_REF] Roşu | An overview of the K semantic framework[END_REF] to perform substitution of Var by Hd in Exp. If the value is true, then the overall result is that of the forAll operation, recursively evaluated on the smaller collection val(Tl); otherwise, the overall result is false.

This relatively simple definition is possible due to a powerful mechanism of K, which automatically generates rewrite rules in order to evaluate arguments of operators declared to be "strict". The actual K grammar for forAll is

Exp ::= Exp ->forAll( Id | Exp ) [strict (1)]
This means that the forAll operator is "strict" in its first argument; that is, this argument will be evaluated before the forAll expression is evaluated.

In order to do this, K automatically generates "heating rewrites" of the form

E 1 ->forAll( V | E 2 ) --→ E 1 ->forAll( V | E 2 )
by which the first computation task becomes the evaluation of the first argument E 1 ; this can generate further computation tasks using the same mechanism, depending on the structure of E 1 (as it is the case with the if-then-else expression in Rule 2). When E 1 is evaluated, "cooling rewrites" of the form:

val( L ) ->forAll( V | E 2 ) --→ val( L )->forAll( V | E 2 )
fill the "hole" left by E 1 . Then, eventually, one of the rules (1-2) finishes the evaluation of the forAll operator.

Conformance Checking A model is well-formed if and only if it conforms to its metamodel, i.e., it is syntactically correct and satisfies the ocl constraints of the metamodel. Specifically, for a dsml, the class diagram of its metamodel defines its syntax, and the ocl constraints define its static semantics. The procedure for verifying that a model is well-formed is referred to as conformance checking.

In the rest of this section we briefly describe conformance checking in K. Syntactical correctness is checked using the K functions specifying the metamodel. The ocl constraints are checked by first "loading" the content of the cell oclConstr into the computation cell k . This is triggered by the following rule:

checkConformance e k e oclConstr
Then, the execution of the ocl semantics generates a computation of the form:

e k e oclConstr • mem • result M model . . . T * ---→ • k e oclConstr • mem v result M model . . . T
in which the result v of the ocl constraints e is placed in the result cell. Finally, a model M satisfies the ocl constraints e if and only if

checkConformance k e oclConstr • result M model . . . T * ---→ • k e oclConstr • mem true result M model . . . T
This provides us with a formal, executable definition for conformance checking.

rewrite pattern (pattern keyword). Patterns are very much like models, discussed in the previous section. The main difference is that rewrite patterns need not be completely specified models; informally speaking, they may match any model that is a "superset" of the pattern. Also, unlike models, rewrite patterns may refer to variables (those declared in the global variable declarations) in addition to constants; and their attributes and references can be local rewrite rules 5 . For example, the time attribute of the activity Y is rewritten from 0 to timeVal, where the latter is a variable, which was chosen to be the value of the time attribute of the process P of our pattern. This means that when the rule is applied, the time attribute of the activity Y gets assigned the value of the time attribute of the process P. Note also the value of the activities reference of P: the meaning of {Y } is a set containing at least the value Y and possibly more. This is in contrast to, e.g., the set {Z}, which means the set containing exactly the value(s) as given. ocl condition (when keyword). This is a condition in the sense of conditional rewrite systems: a rule is applied only when its condition holds after its (global) variables (here, Y and Z) are substituted with the matched (sub)terms. imperative code (then keyword). This is essentially a program composed of assignments, loops, and conditionals. The program starts with the declaration of a list of local variables, distinct from the global variables, which play the roles of usual variables in imperative programs: essentially, they serve for storage of intermediate computed results and as iterators of loops. In our example, the variable r serves as an iterator for the for loop. Regarding assignments, their left-hand side are ocl navigation expressions, i.e., expressions of the form Variable.reference 1 . • • • .reference n , where Variable can be a global or a (previously evaluated) local variable (the latter case appears within the for loop of our example). Their right-hand sides can be arbitrary ocl expressions, including local variables. Finally, note the print statements: their arguments are arbitrary ocl expressions, and they are used to print output -useful for executing, debugging, or verifying kmrl code.

Parsing and processing KMRL with Rascal. The kmrl input defining the operational semantics of a dsml, together with the corresponding metamodel for the dsml's syntax, is transformed into K by a Rascal program in three steps.

In the first step it computes the types of the (global) variables and constants occurring in the rule: in our example, it infers from the metamodel that timeVal is an integer, and that inProgress is an activityState. The second step is a form of "context transformation", also inspired from K but considerably simpler: since the rewriting pattern and its components are typically incomplete, the program completes them with adequately typed variables; for example, the incomplete set {Y, } is completed to {Y, rest}, where rest is a fresh variables that can match any number of set elements. And, finally, the third step consists in separating the rule's rewriting pattern into a left-hand and a right-hand side, which has indeed the effect of turning the pattern into a proper rewrite rule. (Essentially, the right-hand side of a rewrite pattern is a copy of the pattern in which the left-hand sides of the local rewrite rules occurring in it are kept; and symetrically so for the right-hand sides. Those parts of the patttern that are not local rewrite rules appear in both sides, and serve as a rewriting context.)

Let r be a kmrl rule. We denote by lhs(r) and rhs(r) its left-hand and right-hand sides computed by a Rascal program (as described above), by C(r) its condition, and by imp(r) its imperative part. These are translated by Rascal to a K format which we do not present here since it is not essential for understanding. What is important is the the overall translation of the rule r, denoted by K(r): run when(C(r)) update(rhs(r)) apply(imp(r)) run

••• k lhs(r) model
This means that whenever the keyword run (which is by convention the instruction for model execution) is at the top of the k cell, and the model cell matches lhs(r), the run keyword is rewritten into a sequence that evaluates the condition C(r), and, if the condition holds, then it updates the model cell by replacing its contents with rhs(r), it applies the imperative program imp(r) to the result, and, finally, it recursively invokes model execution by reinserting run in the k cell. This effect is obtained by the K semantics of kmrl we now briefly describe.

K semantics of KMRL First, we give the rules for the when clause of K(r). when(true)

• ••• k when(false) K run run ••• k
That is, the when clause disappears (i.e., rewrites to •) when its argument evaluates to true, and it discards the computational tasks corresponding to the current matched rule otherwise. This simplicity is due to the fact that the when operation is strict: its argument (an ocl expression) is a Boolean when the when clause itself is evaluated. The evaluation of the argument consisted in applying the K rules for the semantics of ocl.

Then comes the rule for the update instruction. It simply consists in removing the update keyword from the top of the k cell, and by replacing the content of the model cell by the argument of the (just removed) update instruction:

update(M) • ••• k M model
Finally, there are rules for applying the imperative part imp(r) of K(r). We do not give these rules due to lack of space, but note that, except for assignment (which is quite specific to our present model-based framework) they are standard semantical rules for imperative programs constructs (loops and conditionals).

Execution and Model Checking

The operational semantics that we provide for dsml's semantics is executable, hence, it can directly be used for execution, and, with some user input, for model checking of reachability properties. Execution is here the nondeterministic execution of the (K semantics of) kmrl rules using the K execution engine.

We now illustrate model checking on xspem, whose metamodel and operational semantics rules were shown in Section 2.2. We consider the folllowing reachability problem: is it possible, from the model shown at the bottom of Figure 2, to reach a model where all activities of the model's proper process6 are finished within their expected time limits? A model where all activities of a process P are finished within their expected time limits is characterised by the following ocl expression: P.activities → forAll(a | a.aS = finished ∧ a.tS = ok). To search for such states, we add the kmrl rule in Figure 11 to the set of rules of the semantics of xspem. The rule is not part of the semantics of xspem, but acts like an observer, which runs together with the operational semantics rules, and, when it observes that the expected ocl query holds, it prints (by convention) the string "reached" -actually, it adds this string at the end of the result cell. The problem of finding states satisfying ocl Boolean queries has thus been reduced to searching for K configurations denoting models, reachable from a given initial model-configuration, such that the result cell contains a sequence ending with the string "reached". We have automated this process using a script 7 , that takes the compiled K definition8 of our dsml enriched with the observer rule, launches it in the Maude rewriting engine to search for the shortest solution, and returns the solution, filtered for better readability. Hence, all what users need to write is their observer rule in kmrl: the rest of the process is fully automatic.

Here is, for example, the result of model checking for the property defined by the above observer, as produced by our script (whe have taken advantage of the fact that rules print what they do: starting, clock ticking, and finishing):

["start"] [a : activity] ["tick"] [1] ["tick"] [2] ["tick"] [3] ["tick"] [4] ["tick"] [5] ["finishOk"] [a : activity] ["start"] [b : activity] ["tick"] [6] ["tick"] [7] ["tick"] [8] ["finishOk"] [b : activity]
One thing that can be noticed is that the expected property is indeed satisfied: both activities are finished in time (cf. the ["finishOk"] output printed by their "finishing" rules). Another thing that can be noticed is that b started only when a finished, satisfying the requirement illustrated in the xspem model in Figure 2 by the finishedToStart reference linking b to a via w1. If we replace this link by a e.g., finishedToStart, the shortest solution is a different one, in which the two activitie's starting and finishing events occur in a different order.

Conclusion, Related, and Future Work

We have proposed a formal approach for the definition and analysis of dsmls. The approach uses the K semantical framework, which has shown its efficiency at defining semantics of general progamming languages, and applies it to the mde ingredients used in defining dsmls: metamodels for syntax, ocl for static semantics, models for "programs", and a combined declarative/imperative modeltransformation language for operational semantics of dsmls, which we call kmrl.

The approach was illustrated on xspem, a dsml based on an omg standard. Metamodels, ocl, and models are standard mde concepts, which can be assumed to be familiar to software engineers trained in the basics of mde. We have designed kmrl to re-use as much as possibly mde basics: ocl occurs in both conditions and imperative parts, and the declarative part of kmrl generalises the representation of mde-models. Our hope is therefore that kmrl will be easy to learn by engineers familiar with the basics of mde, which will enable them to formally define their dsmls and to perform formal verifications on them.

We have much benefitted in this work from K's modularity. Each syntactical construct of ocl is defined semantically in terms of a few K rules, and adding new constructions does not alter the semantics of the existing ones. Once ocl was defined, it could be reused as such to define the semantics of conditions of kmrl rules, and, with a few more K rules, we defined the imperative part of kmrl. We have also much benefitted from the flexibility of the general Rascal context-free grammars for parsing, and also from Rascal's powerful primitives for navigating in and transforming abstract syntax trees on the fly.

Comparison with Related Work kermeta [START_REF] Muller | Weaving executability into object-oriented meta-languages[END_REF] is a metamodelling language, which allows (among many other features) users to define the syntax of dsmls using metamodels, and their operational semantics by means of imperative commands of the language (assignments, loops, . . . ). Compared to the imperative kermeta approach to defining dsmls, kmrl also has declarative features (model-rewrite rules), is formally defined, and it allows for formal verification. On the other hand, kermeta is a far richer and more mature language.

The atl language [START_REF] Jouault | ATL: A model transformation tool[END_REF] is a mixed declarative/imperative model transformation language. A formal definition of atl in Maude [START_REF] Clavel | All About Maude, A High-Performance Logical Framework[END_REF] has been given in [START_REF] Troya | Towards a rewriting logic semantics for atl[END_REF]. We took inspiration from atl in this work. Compared to atl, the declarative features of kmrl are more developped: in atl one can only match over one model element, whereas in kmrl we allow for matching over arbitrary model patterns. On the other hand, atl's imperative features are more developped than kmrl's: in atl rules can call each other, and can invoke methods of class diagrams. Another difference is that atl can perform general model transformations (i.e., between different metamodels), whereas kmrl is currently limited to one metamodel.

Several other approaches [START_REF] Boronat | Rewriting logic semantics and verification of model transformations[END_REF][START_REF] José | Formal specification and analysis of domain specific languages using Maude[END_REF][START_REF] Rusu | Embedding domain-specific modelling languages into Maude specifications[END_REF] use the Maude algebraic and rewritingbased formal specification language [START_REF] Clavel | All About Maude, A High-Performance Logical Framework[END_REF]. In these approaches, model transformations (in particular, dsml operational semantics) can only be specified in a declarative manner, by mapping them to Maude equations/rewrite rules. Compared to these approaches, ours also includes imperative features, which are lower-level but allow for better control. The same comparison can be drawn with declarative model transformations based on graph rewriting [START_REF] Taentzer | AGG: A graph transformation environment for modeling and validation of software[END_REF][START_REF] Csertán | VIATRA -visual automated transformations for formal verification and validation of UML models[END_REF].

Finally, the so-called translational approach [START_REF] Combemale | Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification[END_REF] consists in endowing in a dsml with a formal semantics by translating it to a target language that does have a formally defined semantics. For example, xspem has been defined by translation to timed Petri nets [START_REF] Combemale | Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification[END_REF]. Our approach differs in that we define not individual dsmls, but a dsml definition framework (here, the mde-based one). Our approach is thus more general than the translational one, and is more likely to be accepted by nonexperts since it does not require from them specialised knowledge of a target language (for writing a translation from dsml to it). On the other hand, due to its generality, our approach is likely to be less efficient for execution/verification than specialised, "hard-coded" translational ones.

Future Work One can envisage a way to combine the benefits of the translational approach (efficiency) and of ours (generality). It would consist in first having the dsml specialists formally define their language as we propose; then, the definition can serve as reference for translation to specialised languages for, e.g., more efficient execution and verification. If the target language has a formally defined operational semantics, the translation between the formally defined dsml and the target language can even formally be proved correct if needed.

Regarding formal verification, we are now working on scenario verification, which constitutes a high-level validation technique, compatible with the highlevel nature of our dsml definition framework. The framework itself is currently implemented as a loosely coupled set of tools, which requires some knowledge to operate with. We are working on an implementation under Eclipse that will present users a friendly interface for their dsml definitions and analyses.

  activity.allInstances → forAll(x : activity|x.workSequences.size() = 1) undefined tooEarly ok tooLate

Fig. 2 .

 2 Fig. 2. (top): A simplified metamodel for xspem, together with an ocl constraint (bottom) one xspem model that conforms to the xspem metamodel.

Fig. 3 .

 3 Fig. 3. Time-passing rule.

Fig. 4 .

 4 Fig. 4. Starting an activity. The condition is given in the when clause, and imperative code is in the then clause.

Fig. 5 .Fig. 6 .

 56 Fig. 5. Finishing an activity.

Fig. 7 .

 7 Fig. 7. Textual representation of the xspem metamodel from Figure 2 (top).

Fig. 8 .

 8 Fig. 8. Textual representation of the model from Figure 2.

Fig. 9 .

 9 Fig. 9. K Configuration for dsmls

Fig. 11 .

 11 Fig. 11. Observer rule for model checking.

We shall call global variables just "variables" when no confusion with local variables, to be introduced later, can occur. We shall do the same for local variables.

This idea is borrowed from K. The advantage is that produces simple/compact rules.

Remember that we have imposed an ocl constraint stating that there is exactly one proper process -i.e., a process which is not an activity -in each xspem model.

The script can be tested on-line using at https://fmse.info.uaic.ro/tools/.

K definitions are compiled into Maude[START_REF] Clavel | All About Maude, A High-Performance Logical Framework[END_REF] specifications.

The research presented in this paper was supported in part by the DAK project Contract 161/15.06.2010, SMIS-CSNR 602-12516

Operational Semantics

The last ingredient in the definition of a dsml is the definition of its operational semantics. We propose for this the language kmrl (K Model-Rewrite Language), a mixed declarative/imperative language for model rewriting. A glimpse of kmrl has already been shown in Section 2.2, where we informally gave the semantics of xspem using (graphical) model-rewrite rules. To formalise the semantics of dsmls, we need first to formalise the kmrl language itself. We provide it with a textual syntax, checked by a Rascal-generated parser, and with a formal semantics as a set of K rules. Those rules include the rules for the semantics of ocl since ocl is a sublanguage of kmrl.

We now illustrate the overall process with the rule start shown in Figure 4. The textual version of the rule is given in Figure 10. It is composed of four parts:

global variable declaration (forAll keyword). Here, the notion of global variable 4 should be understood as variable in the rewrite-systems terminology: variables match terms, and are replaced by those terms when rewriting is performed; e.g., on our example, the variable Y matches one element of acivities's value (which is a collection). The scope of global variables is the whole rule; they can occur everywhere in the rule.


Pascal Fradet

Alain Girault

Peter Poplavko

SPDF: A Schedulable Parametric Data-Flow MoC

Dataflow programming models are suitable to express multi-core streaming applications. The design of highquality embedded systems in that context requires static analysis to ensure the liveness and bounded memory of the application. However, many streaming applications have a dynamic behavior. The previously proposed dataflow models for dynamic applications do not provide any static guarantees or only in exchange of significant restrictions in expressive power or automation. To overcome these restrictions, we propose the schedulable parametric dataflow (SPDF) model. We present static analyses and a quasi-static scheduling algorithm. We demonstrate our approach using a video decoder case study.

I. INTRODUCTION

Multi-core systems are becoming an increasingly important platform for many embedded system designs. To take advantage of multi-cores, programming languages should express thread-level parallelism. Among such languages, dataflow languages are prominent for many streaming applications [START_REF] Bhattacharyya | OpenDF: a dataflow toolset for reconfigurable hardware and multicore systems[END_REF].

Recent dataflow programming environments support applications whose behavior is characterized by dynamic variations in resource requirements. The high expressive power of the underlying models makes it challenging to ensure predictable behavior. For example, the CAL actor language [START_REF] Bhattacharyya | OpenDF: a dataflow toolset for reconfigurable hardware and multicore systems[END_REF] or Kahn Process Networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF] can express many dynamic applications. However, checking liveness (i.e., no part of the system will deadlock) and boundedness (i.e., can be executed in finite memory) is known to be hard or even undecidable.

This situation is troublesome for the design of high-quality embedded systems. Sufficient criteria for liveness and boundedness have been formulated for less expressive models, which can nevertheless express the core part of many streaming applications. However, such statically analyzable criteria come at the cost of significantly constraining modeling and scheduling. For example, parametrical synchronous dataflow (PSDF) [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF] imposes a hierarchical discipline which restricts scheduling and analysis.

In this paper, we introduce the schedulable parametric dataflow (SPDF) model of computation (MoC) for dynamic streaming applications. SPDF was designed to be statically analyzable for liveness and boundedness, while avoiding the aforementioned restrictions. In Section II, we present a wellknown basic model -synchronous dataflow (SDF) [START_REF] Lee | Static scheduling of synchronous data flow programs for digital signal processing[END_REF] -which is easily analyzable but restricted to static applications. We then introduce our SPDF model as a parametric and dynamic extension of SDF. In Section III, we present the static analyses for boundedness and liveness. Section IV describes the compilation, such as insertion of parameter distribution network and quasi-static scheduling. A video decoding application is presented as a case study in Section V. Finally, Section VI 978-3-9810801-8-6/DATE12/ c 2012 EDAA summarizes our contribution, compares it to related work and hints at future research directions.

II. MODEL OF COMPUTATION

We start from SDF -synchronous dataflow [START_REF] Lee | Static scheduling of synchronous data flow programs for digital signal processing[END_REF] -one of the simplest dataflow MoC. Then, we present our MoC (SPDF) as a statically analyzable extension of SDF with dynamic parametrization.

A. Basic Model: SDF

In SDF, a program is defined by a directed graph, where nodes -called actors -are functional units. The actors have data ports connected by edges which can be seen as FIFO (first-in first-out) channels. The atomic execution of a given actor -called actor firing -consumes data tokens from its incoming edges (its inputs) and produces data tokens to its outgoing edges (its outputs). The number of tokens consumed or produced at a given port at each firing is called the rate. It is denoted as r(π m ) where π m is a port. In SDF, all rates are constant and known at compile time. Fig. 1 shows a simple SDF graph with three interconnected actors A, B and C. Actor A has one input and one output port, whose rates are 2 and 4, respectively.

The state of a dataflow graph is the number of tokens present at each edge (i.e., buffered in each FIFO). Each edge carries zero or more tokens at any moment of time. The initial state of the graph is specified by the number of initial tokens. Edge (C, A) in Fig. 1 has two initial tokens. After the first firing of actor A, the edge (A, B) gets four tokens while the two tokens of (C, A) are consumed.

A major advantage of SDF is that, if it exists, a bounded schedule can be found statically. Such a schedule ensures that each actor is eventually fired (ensuring liveness) and that the graph returns to its its initial state after a certain sequence of firings (ensuring boundedness of the FIFOs). The minimal such sequence is called an iteration.

The numbers of firings of the different actors per iteration are computed by solving the so-called system of balance equations. This system is made of one equation per edge. Consider an edge (X 1 , X 2 ) connecting the ports π 1 and π 2 ; its balance equation is:

#X 1 • r(π 1 ) = #X 2 • r(π 2 ) (1)
This equation states that the number of firings of the producer X 1 , denoted #X 1 , multiplied by its rate r(π 1 ), should be equal to the same expression for the consumer X 2 . For example, the balance equation for edge (A, B) in Fig. 1 is:

#A • 4 = #B • 1.
The existence of solutions of the system of balance equations is referred to as rate consistency. The graph of Fig. 1 is rate-consistent, and the solutions are: #A = 1, #B = 4 and #C = 2. Note that multiplying the solutions by the same positive constant makes another set of solutions. One usually considers only the minimal strictly positive integer solutions which are obtained by eliminating common factors.

The minimal solutions determine the number of firings of each actor per iteration. The next step is to determine a static order -the schedule -in which those firings can be executed. The schedule is obtained by an abstract computation where an actor is fired only when it has enough input tokens. The graph of Fig. 1 can only start by firing A; then, B has enough input tokens to be fired four times, and finally C twice. Since each actor has been fired the exact number of times requested by its solution, a schedule has been found. We represent it as the string AB 4 C 2 where the superscripts denote repetition count. Another valid schedule for the same graph is AB 2 CB 2 C which can also be written as A(B 2 C) 2 .

B. Our model: SPDF

We extend SDF by allowing rates to be parametric while preserving static schedulability. Let P be a set of symbolic variables. SPDF rates are defined by the grammar:

F ::= k | p | F 1 • F 2
where k ∈ N * and p ∈ P Rates are products of positive integers (k) or symbolic variables (p). Optionally, each parameter can be constrained to belong to a specific integer interval ([1, +∞) by default). Fig. 2 shows a simple SPDF graph where the actors have constant or parametric rates (e.g., p • q for the input rate of C).

1 B A set q[p] set p[1] q C 1 2 pq 2p Fig. 2. A simple SPDF graph
Unlike the rates of SDF graphs which are fixed at compile time, the parametric rates of a SPDF graph can change dynamically. The changes of each parameter are made by a single actor called its modifier. By default, a parameter can be changed between iterations. In SPDF, a modifier may change a parameter more often using the annotation "set p[α]" where p is the parameter to be set and α is the exact (possibly symbolic) number of firings of the modifier between two parameter changes. In Fig. 2, A and B are the modifiers for p and q; they may change their value every single and p firings, respectively.

Definition 1: A SPDF graph is a tuple (G, P, i, d, r, M, α), where:

• G is a directed connected graph (A, E) with A a set of actors and E ⊆ A × A a set of directed edges; • P is a set of parameters;

• i : E → N associates each edge with its number of initial tokens; • d : P → 2 N * returns the interval of each parameter;

• r : A × E → F returns for each port (represented by an actor and one of its edges) its associated (possibly symbolic) rate; • M : P → A and α : P → F return for each parameter its modifier and its change period, respectively.

III. STATIC ANALYSIS FOR SPDF

This section presents the three static analyses needed to ensure boundedness and liveness of an SPDF graph. In Section III-A, we check rate consistency by adapting the analysis of SDF to SPDF. Conditions for consistency and solutions of balance equations are computed in terms of symbolic expressions. In Section III-B, we check that the change periods of each parameter are safe. Rate consistency and parameter change safety ensure boundedness. Section III-C completes the analysis chain by checking for liveness.

A. Rate Consistency

As in SDF, we check the rate consistency of a SPDF graph by generating the associated system of balance equations. This system must be shown to have a solution for all possible values of parameters. When parameters are modified only between iterations, rate consistency ensures boundedness.

We generalize the algorithm for solving the balance equations in SDF presented in [START_REF] Bhattacharyya | Software Synthesis from Dataflow Graphs[END_REF] to SPDF by doing the same operations with symbolic factors. That algorithm relies on multiplication, division and greatest common divisor (gcd) of rates. These operations are easily expressed on F by putting symbolic expressions on the form:

k 0 • k 1 • k 2 • • • prime decomposition • p 1 • p 1 • • • p 1 the power of p1 • p 2 • p 2 • • • p 2 the power of p2 . . .
The minimal solutions for all actors are found by eliminating all the prime or parameter factors common to all solutions.

If the undirected version of the SPDF graph is acyclic, a solution always exists and will be found by the above computation. When the SPDF graph contains an undirected cycle, the graph may be rate inconsistent. There is, however, a necessary and sufficient condition for the existence of solutions. Each undirected cycle X 1 , X 2 , . . . , X n , X 1 where p i and q j denote the rates of edge (X i , X j ) should satisfy the following condition:

(Cycle condition) p 1 • p 2 . . . • p n = q 1 • q 2 . . . • q n
This condition enforces that any factor encountered on an "output" port of a cycle should have a symbolically identical counterpart on an "input" port on this cycle.

Theorem 2 (Consistency): An SPDF graph is rate consistent if its undirected cycles satisfy the cycle condition [START_REF] Fradet | Spdf: A schedulable parametric dataflow graph model[END_REF].

For example, the graph of Fig. 2 is consistent since its only cycle A, B, C, A satisfies the cycle condition which is 2p

• q • 1 = 2 • 1 • pq. The minimal solutions are #A = 1, #B = 2 • p and #C = 2, yielding the schedule AB 2p C 2 .
The specified algorithm either yields for each actor its (symbolic) solution, or returns an unsatisfied cycle condition that can be used by the programmer to fix his SPDF graph.

B. Parameter Change Safety

It is always safe to change parameter values between graph iterations [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF]. Indeed, the rate consistency and liveness analyses ensure that the graph is bounded and live for any value of the parameters. Since the graph returns to its initial state after each iteration, all parameters can be modified at these stages. Nevertheless, it is sometimes useful to change the parameters more often, i.e., during an iteration. SPDF allows the programmer to specify a faster period using the "set p[α]" annotation. Yet, not all periods are safe and their consistency must be checked. Consider, for instance, actor B that modifies q in Fig. 2. The period 1 would not be safe since it is only after p firing of B that C can consume its pq tokens. The rate pq would not be well defined if q can change p times before C is fired. On the other hand, the period p is safe since the iteration can be written A(B p C)(B p C), with q being changed after each sequence (B p C).

The criterion ensuring that parameter modification periods are safe relies on the notions of influence, regions and local iterations. Intuitively, the criterion states that a parameter can be modified once per local iteration of the region it influences. For Fig. 2, it can be shown that the region of influence of q consists of actors B and C and that q can be changed after each local iteration (B p C), that is, after p firings of B.

Definition 3 (Influence): An edge e = (A, B) is influenced by a parameter p, denoted Infl (e, p), if p appears in the rates of e or in the solutions of the balance equations of its source and sink actors. Formally,

Infl (e, p) ⇔ p ∈ #A ∨ p ∈ #B ∨ p ∈ r(A, e) ∨ p ∈ r(B, e)
where p ∈ F if p occurs in the symbolic expression F.

The region of influence of a parameter is the subset of edges it influences. Since an edge is a relation between actors, a region also specifies a subset of actors.

Definition 4 (Region): The region of edges R(p) influenced by p is defined as: R(p) = {e | Infl (e, p)}

We will sometimes abuse notation R to denote also the set of actors connected by the edges of the region. For example, the region of influence of q in Fig. 2 is R(q) = {(B, C)} and the actors in this region are {B, C}.

The solutions of the system of balance equations are global solutions in that they define the number of firings for the global iteration of the whole graph. Local solutions are solutions for a subset of actors; they denote a nested iteration.

Definition 5 (Local solutions): Let A be the set of actors of an SPDF graph and #X be the global solution of X. The local solution of X in the subset {X 1 , . . . , X n } ⊂ A, denoted # L X, is obtained by dividing the global solution of X by the greatest common divisor: # L X i = #Xi gcd(#X1,...,#Xn) .

For example, the global solutions for Fig. 2 are #A = 1, #B = 2p and #C = 2, forming the global iteration AB 2p C 2 . The gcd of #B and #C is 2 and the local solutions for the subset {B, C} are # L B = p and # L C = 1. After one local iteration B p C, all the edges influenced by q return to their initial state. Therefore, q can be changed after each such local iteration, hence after p firings of B, as specified by the "set q[p]" annotation.

Regions of influence of a given parameter can overlap (i.e., have common edges). Each local iteration of such region may entail firing the same actor a different number times. Such overlapping regions must be grouped so that the modification periods of their parameters are checked on the same subset of actors. Regions are then generalized to a subset of parameters P ′ as follows: R(P ′ ) = {e | ∃p ∈ P ′ , Infl (e, p)} When a region R(P 2 ) is included within another region R(P 1 ), the periods of the parameters in P 2 can be checked on R(P 2 ). The local iteration of R(P 1 ) will always involve one or several local iterations of the inner region. Hence, the changes of parameters from P 1 are always done between local iterations of R(P 2 ) and are therefore safe for both regions.

Before checking the parameter modification safety criterion, we structure the set P of all parameters into a hierarchy tree of sets of parameters P i such that:

• P is partitioned into non-empty partitions P i that are placed at different nodes and leafs of the hierarchy; • the region of a set P i is strictly included in the region of its parent P j (i.e., R(P i ) ⊂ R(P j )); • the regions of two sets P i and P j which are not ancestor or descendant of each other are disjoints. This structuring process is based on two basic steps:

• (Decomposition) the first step decomposes the current set of edges (initially E) into disjoint regions. Consider the relation e 1 ≍ e 2 which holds if there exists a parameter influencing both edges e 1 and e 2 . Then, disjoint regions are the connected components of the graph of the ≍ relation. Each disjoint set of edges corresponds to a region of a disjoint set of parameters; • (Nesting) the second step finds, for each such independent region R(P), the largest subset P ′ ⊂ P such that R(P ′ ) ⊂ R(P -P ′ ). The set P -P ′ will be the root of the (sub-)tree that will be built by iterating the process (decomposition and nesting) on P ′ . This process ends when P ′ = ∅. Fig. 3 represents a graph with two hierarchy levels: the parent level P 1 = {p} and the child level P 2 = {q}. The parameter p influences all edges whereas q influences only (A, D) and (D, C), hence R(P 2 ) ⊂ R(P 1 ). We can now state the criterion for parameter modification safety.

Definition 6 (Data Safety): An SPDF graph is data safe if, for each parameter p and its hierarchy node P i such that p ∈ P i , every actor X j in R(P i ) is such that #X j is a multiple of #M (p)/α(p).

This criterion ensures that when a parameter takes a new value between two local iterations of its hierarchy level, all the data edges come back to their initial state. In Fig. 3, we have q ∈ P 2 , #M/α = #A/1 = 2, and R(P 2 ) = {A, C, D}. The solutions for the actors in R(P 2 ) are all multiples of 2: #A = 2, #C = 2p and #D = 2pq. The annotation "set q[1]" in A is thus data safe. Definition 7 (Period Safety): An SPDF graph is period safe if, for every pair of parameters p and q such that #M (q) depends on at least one parameter of the hierarchy node of p, #M (q)/α(q) is a multiple of #M (p)/α(p).

A D C R(p) R(q) set q[1] set p[2]
This criterion ensures that every modifier is contained in at least one region whose local iterations never finish when a period of that modifier is not yet completed. E.g., the graph of Fig. 2 is period-safe because even if the solution of M (q) depends on p (#M (q) = #B = 2p), #B/α(q) = 2 is a multiple of #M (p)/α(p) = 1, so the criterion is satisfied.

Theorem 8 (Boundedness): If an SPDF graphs is rate consistent, data safe and period safe, then all data edges and periods come back to the initial state at the end of a global iteration. Hence it can be scheduled in bounded memory.

C. Liveness

If the directed SPDF graph is acyclic it is trivially live: there exist actors that can always fire, thus allowing other actors to fire, and so on until the iteration is complete. However, if there exists a directed cycle, we must check that each cycle contains enough initial tokens. For example, if the (C, A) edge in Fig. 2 had only one token, then A (and therefore B and C) could never fire. Checking the liveness of SDF graphs is done by computing an iteration by abstract execution. It is not clear whether such an approach is applicable to SPDF. Instead, we present a sufficient condition on cycles.

Definition 9 (Live cycle): Consider a cycle consisting of n actors X 1 , X 2 , . . . X n and n edges e 1 = (X n , X 1 ), e 2 = (X 1 , X 2 ), . . . e n = (X n-1 , X n ). We say that the cycle is live if ∃1 ≤ k ≤ n such that i(e k ) ≥ r(X k , e k ) • #X k , i.e., there is an edge with enough initial tokens to fire an actor the needed number of times to complete the iteration.

If r(X k , e k )•#X k is a symbolic expression, the inequality is checked using the maximum values of the parameters involved. If one of the parameters does not have a declared maximum, then the inequality is considered false. In Fig. 2, the cycle is live since i(C, A) = 2, r(A, (C, A)) = 2, and #A = 1.

Definition 10 (User): A user U of a parameter p is an actor different from M (p) such that p occurs in #U or in the rate of one of the ports of U .

Theorem 11 (Liveness): A rate-consistent and safe SPDF graph is live if each of its cycles is live and if, for each parameter, there is path from the modifier to all the users without initial tokens [START_REF] Fradet | Spdf: A schedulable parametric dataflow graph model[END_REF].

The second requirement ensures that the parameter communication from the modifier to the users does not introduce non-live cycles. Liveness analysis either succeeds or returns to the programmer the faulty cycles (i.e., with not enough initial tokens) or the faulty modifier-user pairs. We could use, as in [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF] [5], less restrictive criteria using local solutions in strongly connected subgraphs. We skip this possibility here for space and simplicity reasons.

IV. COMPILATION

We first show how to transform any safe SPDF graph into a graph which can be scheduled in bounded memory by dynamic scheduling (Section IV-A). Then, we describe how to generate a quasi-static schedule (Section IV-B).

A. Parameter Communication for Bounded Scheduling

The critical aspect for scheduling SPDF graphs is the communication of the values of parameters from the modifiers to the users. We implement this communication by adding extra actors, edges, and ports, forming a parameter distribution network (PDN), in such a way that the SPDF graph remains rate consistent and safe. The PDN joins M (p) to all the users of p. It is inserted in three steps.

The first step adds to M (p) a new output port, and to each user a new control port, respectively to send and to receive the successive values of p. Control ports behave exactly as in BDF [START_REF] Buck | Scheduling dynamic data-flow graphs with bounded memory using the token flow model[END_REF]: each actor must read input tokens from all its control ports before reading tokens from its regular data ports. The second step adds a new actor E p , called the emitter of p, and a new edge e = (M (p), E p ), such that r(M (p), e) = 1 and r(E p , e) = α(p). Among the α(p) tokens it receives, E p transmits only the first one, the one that contains the new value of p. We refer to E p as a downsampler (↓). This is illustrated in Fig. 4.

sj 1 1 U 2 1 1 P1 P2 P3 1 1 U 1 11 1 1 P1 P2 P3 {S j }1 1 P1 P2 P 1 1 1 1 P1 P2 P1 'add to the set' R 1 R 2 1 R 3 1 f u1 f u2 1 1 ↓ ↓ ↓ ↓ M(p)1 1 E p 1 1 1(p)
In general, E p fires once per certain number of firings of the users, so each user should receive the same value of p repeated a certain number of times. The third step implements this requirement using upsamplers (↑) that repeat every input token a given number of times. This step depends on the region hierarchy.

Definition 12 (User Location): A user X of p is said to be located w.r.t. to p at the lowest hierarchy level that contains p or a parameter that occurs in #X.

Definition 13 (Edge Location): An edge is said to be located in the hierarchically lowest region that contains it.

The order in which the users are connected to the emitter is defined by their hierarchal location. For parameter p contained in hierarchy node P k the users can be located in the node P k itself or lower in the hierarchy (see Fig. 4).

It can be shown that the output edge of p's emitter is located in a higher region than the location of any user of p. Let R 1 be the region of the p's emitter output and R N be one of the regions where p is used; with the hierarchy path: R 1 , R 2 . . . R N (see Fig. 4, where N = 3).

Definition 14 (Local iteration w.r.t. a larger region): The local iteration count of a region R ′ in the context of a larger region R ′′ , R ′ ⊂R ′′ , is defined as gcd{#X|X∈R ′ } gcd{#X|X∈R ′′ } . This local iteration count gives the number of iterations of R ′ per each iteration of R ′′ .

Let us calculate the upsampling factor f U that is common for all users in R N . Let f R be the number of local iterations of R N w.r.t. R 1 and f E be the local solution for E, definition 6 implies that f R is a multiple of f E and we write

f U = f R /f E .
In general, f U may include parameters from different regions. So, to preserve the parameter safety, instead of one upsampling actor we need an actor chain (U k ) k=1...N -1 with one actor per region (see Fig. 4). Their upsampling rates are obtained by considering f U as :

f U = f u1 • f u2 • • • f u(N -1) .
One can show that f uk = f rk /f ek . The values f rk are a splitting of f R calculated for each k as the number of local iterations of R k+1 in the context of R k . The values f ek are a splitting of f E calculated by f ek = gcd (f rk , f Ek ), where

f E1 = f E and f Ek = f Ek-1 /f ek-1 , for k = 2 . . . N .
Having thus inserted the upsampling chain to region R N for each internal user X j , we insert an extra upsampling actor S j with upsampling rate s j equal to local solution # L X j in the context of region R N (see Fig. 4).

Our PDN insertion algorithm [START_REF] Fradet | Spdf: A schedulable parametric dataflow graph model[END_REF] first inserts all the emitters, then visits the hierarchy nodes P i and connects the users in R(P i ) to the emitters as described above. The hierarchy tree is visited in a bottom-up order. Although U k and S j are new users, they can be located only in the current or higher nodes, so, in the end, all users are connected.

After inserting the PDN, the final step is to shortcut all the samplers with rate 1. The graph of Fig. 2 with its PDN is shown in Fig. 5. We obtain a bounded and safe SPDF graph where all communications are done via FIFOs. It can be dynamically scheduled in bounded memory [START_REF] Parks | Bounded scheduling of process networks[END_REF].

B. Quasi-static scheduling

In SPDF, since the firing counts of some actors can be parametric, so is the schedule, which is said to be quasistatic [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF]. Currently, our quasi-static scheduling algorithm requires that all parameters p i can be ordered such that their corresponding modifiers M (p i ) with periods α(p i ) are related by: #M (pi+1) α(pi+1) = f i • #M (pi) α(pi) , for some f i ∈ F. Observing that #M (pi) α(pi) denotes the modification count of p i during a global iteration, we can expect our requirement to hold often in practice. A typical streaming application can be represented by nested loops where each parameter is modified exactly once at a certain loop level. The ordering of parameters corresponds to the different loop levels.

Our liveness criterion implies that we can ignore the edges with initial tokens and consider the corresponding acyclic graph. First, for the source (i.e., non-PDN) part of the graph, we generate a string composed of the actors of that graph sorted topologically, e.g., ABC for Fig. 5. In this string, we replace every actor X by the wrapper:

p ↑ 1 2 ↑ 1 2 B A set q[p] set p[1] C 2 ↑ 2p 1 p 2p q pq 1 1 1 1 ↓ 1 p 1 1 p q 1 1 1 q 1 p p
(set p i1 ; (set p i2 ; . . . (set p i N ; X f ′ N +1 ) f ′ N . . . ) f ′ 2 ) f ′ 1
where p i k (k = 1 . . . N ) are parameters used or modified by X; i k are the increasing indexes of parameters in the above ordering; 'set p i ' sets a new parameter value for the given actor;

f ′ 1 = #M (p 1 )/α(p 1 ); f ′ k = #M (pi k )/α(pi k ) #M (pi k-1 )/α(pi k-1 ) for k = 2 . . . N ; f ′ N +1 = #X
#M (pi N )/α(pi N ) . For Fig. 5, we produce (set p; A; ) (set p; (set q; B p ) 2 ) (set p; (set q; C) 2 ).

Finally, we introduce modifier-to-user communication statements, equivalent to PDNs [START_REF] Fradet | Spdf: A schedulable parametric dataflow graph model[END_REF]. The modifier is implicitly connected to each user by a separate queue. It writes to all the queues with a single "push p i ". Each user reads the parameter values by a "pop p i ". In the wrapper for actor X, we replace the "set p i " by "push p i " if X is the modifier or by "pop p i " otherwise. The push are moved after the actor invocation, because the actor as modifier has to compute the value to be pushed. In our running example, we get: (A; push p) (pop p; (B p ; push q) 2 ) (pop p; (pop q; C) 2 ).

V. CASE STUDY

We have applied SPDF to realistic case studies provided by an industrial partner. Figure 6 shows a SPDF model for a video decoder. The actor "input" reads the coded input frame and triggers a variable-length decoder "vld" for the 100 macroblocks of the frame. Once per frame (period 100) "vld" determines parameter p indicating whether the frame uses motion compensation. The actor "mv" determines whether the current macroblock has motion vectors (parameter t). If both conditions hold (p • t), motion compensation is performed by the actor "mc". The actor "vld" triggers the calculation of four luminance blocks, "lum", each one computing an l indicating whether it is coded. For coded blocks, inverse discrete cosine transform (IDCT) is performed by the actor "l-idct". The actor "vld" also determines whether chrominance is coded in macroblock (parameter c). If so, it triggers the execution of IDCT, "c-idct", followed by upscaling, "upsc", which builds four chrominance blocks out of one. Finally, the four luminance and chrominance blocks of the macroblock are converted one-by-one to RGB color format by the actor "color" and sent to the output frame. For each 100 macroblocks, the output frame expects 400 blocks.

Concerning rate consistency, the cycle condition is true for three undirected cycles, so the balance equation algorithm succeeds. Concerning safety, our hierarchy computation algorithm finds three disjoint nodes with parameter sets P 1 = {p, t}, P 2 = {l}, and P 3 = {c}. The video decoder does not have directed cycles and the modifiers are located upstream to the users, so the liveness criterion holds. Then, the PDN is inserted, shown in grey in Fig. 6. Finally, the quasi-static scheduler examines the periods of the modifiers and sorts the parameters: (p (modified ×1/frame), c (×100 more), l, t (×4 more)). Applying our algorithm, we obtain the following schedule: input ((vld; push c) 100 ; push p) (pop p; (mv; push t) 400 ) (pop p; (pop t; (mc) pt ) 400 ) ((lum; push l) 400 ) ((pop l; (l-idct) l ) 400 ) (pop c; (c-idct) c ) 100 (pop c; (upsc) c ) 100 (pop c; (pop l; pop t; color) 4 ) 100 output Actually, all the parameters (p, t, l, c) have been encoded as booleans. For space reasons, we have not presented this extension, but the whole methodology presented in this paper applies to this example without restrictions [START_REF] Fradet | Spdf: A schedulable parametric dataflow graph model[END_REF].

VI. CONCLUSIONS

We presented SPDF, a novel MoC for parametric streaming applications enabling static analysis and scheduling. We for-mulated sufficient and general static criteria for boundedness and liveness. In SPDF, parameter changes are allowed even within iterations. Their safety can be checked and their implementation is made explicit. All this was possible because we could manipulate and compare dynamic values by well-defined static operations on symbolic expressions. The same holds for quasi-static scheduling, which is the first step towards code generation for multi-core systems.

The most closely related MoC is PSDF [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF], which requires to manually find the hierarchy levels and enclose them into hierarchical actors, e.g., four levels for Fig. 6. With PSDF, the analysis is not completely static, as [START_REF] Bhattacharya | Parameterized dataflow modeling of DSP systems[END_REF] applies a run-time analysis at hierarchy boundaries. The hierarchy analysis proposed in [START_REF] Neuendorffer | Hierarchical reconfiguration of dataflow models[END_REF] requires significant manual help. The Scenario-Aware Data-Flow (SADF) MoC [START_REF] Stuijk | Scenario-aware dataflow: Modeling, analysis and implementation of dynamic applications[END_REF] extends SDF with performance analysis; yet, SADF does not define any boundedness analysis if hierarchy is present. The Variable-Rate Data-Flow (VRDF) MoC [START_REF] Wiggers | Buffer capacity computation for throughput constrained streaming applications with data-dependent inter-task communication[END_REF] introduced support for frequent changes of actor rates. However, VRDF imposes strong structural constraints on the graph. In particular, each production of p tokens must be matched by exactly one consumption of p tokens, and these pairs must be well parenthesized in the VRDF graph.

Multiprocessor scheduling for SPDF is an obvious and important extension of our work. Other important future work is SPDF scheduling with dynamic voltage and frequency scaling and performance-memory trade-off exploration. We also intend to explore other forms of dynamicity, such as dynamic graph reconfigurations, while preserving static schedulabilty.

data port π 2 Aπ 1 Fig. 1 .

 211 Fig. 1. A simple SDF graph.

Fig. 3 .

 3 Fig. 3. An SPDF graph with two hierarchy levels: P 1 = {p}, P 2 = {q}.

1

 1

1 Fig. 4 .

 14 Fig. 4. Communication of a parameter from the modifier to the users.

Fig. 5 .

 5 Fig. 5. The SPDF graph of Fig. 2 with its PDN.

Fig. 6 .

 6 Fig. 6. Video decoder (compiler-inserted elements shown in gray).

ACKNOWLEDGMENTS

Thanks are due to Ali-Erdem Ozcan for providing the case study and numerous discussions.