Benoît Combemale

Xavier Crégut

Pierre-Loïc Garoche

Xavier Thirioux

Francois Vernadat

A Property-Driven Approach to Formal Verification of Process Models

Keywords: Metamodelling, Properties Validation, Verification, Temporal OCL, Process Model, Petri Nets, LTL, Models Semantics, Model Transformation

More and more, models, through Domain Specific Languages (DSL), tend to be the solution to define complex systems. Expressing properties specific to these metamodels, and checking them, appear as an urgent need. Until now, the only complete industrial solutions that are available consider structural properties such as the ones that could be expressed in OCL. There are although some attempts on behavioural properties for DSL. This paper addresses a method to specify and then check temporal properties over models. The case study is SIMPLEPDL, a process metamodel. We propose a way to use a temporal extension of OCL, TOCL, to express properties. We specify a models transformation to Petri Nets and LTL formulae for both the process model and its associated temporal properties. We check these properties using a model checker and enrich the model with the analysis results. This work is a first step towards a generic framework to specify and effectively check temporal properties over arbitrary models.

Introduction

Domain specific approaches tend to be the next approach for specifying complex systems, giving the appropriate abstraction. They can be easily built by domain experts and can then be integrated in generic toolkits and frameworks. Nowadays, there exists a bunch of environments allowing to define DSL (EMF1 , GME2 ...) mainly focusing on abstract and concrete syntaxes.

Once a metamodel specific to a particular domain has been defined, one wants to express properties that have to be verified for models of this DSL. Such extensions are usually expressed in OCL and describe structural properties of the model. Initially OCL constraints were applied to UML models. Therefore many works and tools have been designed in order to verify these constraints. Tools developed for UML have been adapted to DSL.

However, for behavioural properties, there is a lack of effective works that define all the steps from the property specification to its effective verification. Numerous current projects, such as Topcased 3 , consider these problematics as a main topic.

The paper introduces a property-driven approach for specifying and checking temporal properties. The case study is process engineering. Our approach can be described as simple steps. We first characterise the properties. Then process states must be identified. The DSL metamodel is then extended to represent these states. We adapt an OCL temporal extension, formalized using a LTL semantics [START_REF] Chaki | State/event-based software model checking[END_REF], to represent our temporal properties. The properties are then checked in another formalism: Petri nets. A model transformation to Petri nets is given and allows to apply model checking on an observational abstraction of the trace semantics of the given model with respect to the properties. Finally the result of the analysis is used to enrich the model with properties information.

This paper gives the following contributions:

-we propose a property-driven approach to identify dynamic states of process models; -we introduce a temporal extension of OCL based on process states; -we translate temporal constraints into LTL constraints on the Petri nets; -we propose an observational trace semantics for SIMPLEPDL; -we define SIMPLEPDL denotational semantics though a mapping to Petri nets; -we define a front end for the Tina model checker.

This paper is organised as follows: the second section introduces our DSL, a process metamodel, as well as the natural expression of the user needs for models validation. The third section develops our proposition on our case study. The fourth section considers related works then the last section concludes.

Case Study: Process Model Validation

Our contribution is introduced through a modelling language example on which we would like to express a set of properties that have to be verified on all possible models. Our DSL is a simple process description language: SIMPLEPDL.

We first introduce the domain concepts of SIMPLEPDL and then the kind of properties we want to check on models. The properties we are interested in are properties specific to our DSL that must be satisfied for every model of our metamodel. In fact, our approach of verification is driven by those properties. Properties allows to caracterise SIMPLEPDL models states and then refine the metamodel to capture them.

SIMPLEPDL

SIMPLEPDL is an experimental language for specifying processes. The SPEM standard (Software Process Engineering Metamodel) [START_REF]Software Process Engineering Metamodel (SPEM) 2.0 Specification[END_REF] proposed by the OMG inspires our work 4 , but we also take ideas from the UMA metamodel (Unified Method Architecture) used in the EPF Eclipse plug-in 5 (Eclipse Process Framework), dedicated to process modelling. It is simplified to keep the presentation simple.

The SIMPLEPDL metamodel is given in Figure 1. It defines the process concept (Process) composed of a set of work definitions (WorkDefinition) representing the activities to be performed during the development. One workdefinition may depend upon another (WorkSequence). In such a case, an ordering constraint (linkType) on the second workdefinition is specified, using the enumeration WorkSequenceType. For example, two workdefinitions WD1 and WD2 linked by a precedence relation of kind finishToStart specify that WD2 will be able to start only when WD1 is finished (and respectively for startToStart, startToFinish and finishToFinish). SIMPLEPDL does also allow to explicitly represent resources (Resource) that are needed in order to perform one workdefinition (designer, computer, server, . . . ) and also time constraints (min time and max time on WorkDefinition and Process) to specify the minimum (resp. maximum) time allowed to perform the workdefinition or the whole process.

One can remark that, for the sake of brevity, some concepts are not presented here such as products (WorkProduct) that workdefinitions handle, or roles (Role) that can be assimilated to resources.

Properties

We now present the different kinds of properties specific to the proposed metamodel: structural ones, temporal ones and quantitative ones. We will particularly develop the second kind as a core concept for the rest of the paper.

Structural properties:

The expressivity of metamodelling languages (i.e. meta-metamodels) does not allow to formally capture the whole set of the language properties, i.e. the axiomatic semantics. They mainly capture the cardinalities constraints

In programming languages, the axiomatic semantics is usually based on mathematical logics and expresses a proof method for some construction properties of a language [START_REF] Cousot | Methods and logics for proving programs[END_REF]. It can be very general, such as Hoare triples or restricted to ensure construction consistency (e.g. typing).

In a modelling language, this second kind of use is expressed using well formedness rules at the metamodel level. Such rules have to be realised by all models that are conform to this metamodel. One can check these rules by static analysis on models.

In order to express the rules, the OMG advocates the use of OCL [START_REF]UML Object Constraint Language (OCL) 2.0 Specification[END_REF][START_REF] Warmer | The Object Constraint Language: Getting Your Models Ready for MDA[END_REF]. Applied at the metamodel level, OCL can add properties, mostly structural, that could not have been captured by the metamodel definition. It is a mean to precise the metamodel semantics by limiting possible conforming models.

There is an example of such a constraint:

One WorkSequence could not have the same WorkDefinition as source and target.

That can be formalised as context WorkSequence inv : self.predecessor <> self.successor

In order to check that a particular model satisfies these constraints, one can use an OCL checker such as USE [START_REF] Richters | Validating UML models and OCL constraints[END_REF], OSLO 6 , or EMFT 7 .

Temporal properties: Many properties have to be satisfied in every model execution. The expert of the domain will formalise them when defining the metamodel. In our process metamodel, any workdefinition can be started and then be finished. One can then ask, and therefore check, whether a given process model effectively terminates, i.e. that every workdefinition in it finishes. Taking into account time and resources, some new properties appear that are independent of any model. For a given set of resources, described in the model, does the process terminate ? Is it possible to satisfy every real time constraints expressed on the workdefinition (attributes min time and max time) ? We could also express temporal properties depending on the capability for a workdefinition to suspend its work and free its resources to share them temporarily with other workdefinitions.

Quantitative properties: The aim of such properties is to describe or compute critical paths of executions in terms of minimal or maximal resource consumption. WCET 8 or schedulability are typical examples of quantitative properties. For instance, time and memory are standard resources the usage of which one would wish to measure. In this respect, a consumption (and production) model has first to be set. In simple situations, a discrete and finite model may fit the needs, as it is the case when we focus on a single kind of resource, with a fixed and finite number of instances. Memory requirements alone usually fall in this simple class and could be checked with off-the-shelf model-checking techniques for discrete models, nevertheless with possible minor adaptations. Yet, for more involved models and resources, in order to precisely represent what is happening, we may find it mandatory to write down quite general arithmetical constraints or to handle continuous quantities (as in real-time systems specifications for instance). As discussions about relevance of such models and their verification issues are quite complex and out of the scope of this present work, we choose for the time being to simply rule out quantitative properties and postpone their introduction for future works. Thus, we stick to the presentation of the overall methodology without delving upon details.

Dynamic Informations & Property-Driven Approach

Expressing temporal properties that have to be checked on each model execution implies the existence of an operational semantics that is not expressed within a metamodelling language such as the MOF.

In our case, the execution of a process model consists in performing the different work definitions of the process. When executing a model, every work definition must be started and the overall process must finally reach a state where all of them are in the state finished. The real semantics can be arbitrary complex, and sometimes non computer-representable in case of complex continuous systems.

Our previous works have investigated the use of operational semantics [START_REF] Benoit Combemale | Towards a rigorous metamodeling[END_REF] and translational semantics [START_REF] Benoit Combemale | Sim-plePDL2Tina : Mise en oeuvre d'une Validation de Modèles de Processus[END_REF]. In this paper we present a generic approach to define the abstract dynamic semantics, a semantics of observable events, built upon the properties expressed at the metamodel level.

The temporal properties expressed for every model conform to the metamodel are built over a notion of states. The formal semantics associated to the system can be seen as the set of maximal finite traces which elements are model states. If the metamodel has a well defined operational semantics, it can be easily expressed as a modification of instances' attributes or a modification of the topology (dynamically creating or killing instances). On the contrary, if the associated semantics is not formally defined, the states characterised by properties allow to define an observable operational semantics. Following this idea, if state properties rely on notions that cannot be directly expressed in the model (classical OCL queries), then the metamodel must be enriched to express these notions. The dynamic operational semantics, i.e. the Kripke structure that allows to build trace semantics, must then be approximated by defining transition between characterised states. It is the work of the domain expert to describe them. This approach has mainly three advantages:

-it gives a method to define a formal semantics for metamodel that could not always initially describe it; -this approach is incremental: the domain expert can specify a property, that characterises new states. Then he will extend the metamodel to represent this new dynamic information. The expert can then introduce another property and extend again the metamodel. -it allows to easily define an "observable" approximation of the trace semantics. One such approach allows to check the properties defined, because the semantics were defined depending on the needs expressed by these properties. It can also help in defining a minimal abstract semantics that gives access to formal tools allowing to check properties on a reasonably-sized state space.

3 An Approach to Validation through Petri Nets and LTL

In this section, we will follow all the steps that allow us to express temporal constraints on our SIMPLEPDL metamodel.

Characterising Properties

This first step must be realised by the expert. As expert of processes, we say that every SIMPLEPDL model must verify the following properties. We separate them in two classes: universal properties that have to be satisfied by every execution and existential properties that must be true in at least one execution. Our universal properties are: (1) every workdefinition must start, (2) all started workdefinitions must finish, (3) once a workdefinition is finished, it has to stay in this state, (4) a workdefinition is able to start depending on worksequences constraints. All workdefinitions that are linked to it using a startToStart worksequence are started. Reciprocally all workdefinitions that are linked to it using a finishedToStart worksequence are finished.

The same kind of properties apply for finishing each workdefinition. Our existential properties are: (1) every workdefinition must take more than min time and less than max time to be performed, (2) the overall process is able to finish, i.e. when all workdefinitions are finished in time (i.e. between min time and max time).

Characterising States

The second step consists in characterising different states for the metamodel elements from the properties. From the aforementioned temporal properties, we can identify two orthogonal ideas for the workdefinition element. First, a workdefinition can be not started, started and finally finished. Secondly, there is a notion of time and clock associated to each workdefinition; but this time is only relevant for transition enabling conditions (in our case transitions that start and finish a workdefinition) and is not explicit in state properties. Thus it can be represented into the finite set of states {tooEarly, ok, tooLate}. This second orthogonal idea is only relevant when the progress is finished. Therefore we add a fourth state: notFinished.

Extending the Metamodel to Represent Dynamic Information

We now have to express these states by extending the WorkDefinition elements in order to introduce attributes that reflect dynamic information, i.e. the state of the current workdefinition. We choose to add three variables: state ∈ {notStarted, started, f inished}, time state ∈ {notFinished, tooEarly, ok, tooLate} and clock ∈ R + . An observational abstraction of the operational semantics of our processes with respect to our properties can now be defined.

The expert has again to formalise the initial states and the transition relation. In our case, it is quite natural: the initial states are the singleton {w → (notStarted, notFinished)| w ∈ W D}. We define the transition relation for one workdefinition in W D in Figure 2.

Expressing Temporal Properties : Temporal OCL

A few temporal extensions of OCL have already been proposed in a UML context (see related works section). We have chosen the proposal of [START_REF] Ziemann | An extension of OCL with temporal logic[END_REF] for two main reasons:

1. The semantics of the temporal expressions is formally defined on a trace semantics. Such traces are finite sequences of system states, describing a snapshot of the running system. Even if this work was initially defined on UML models, the trace semantics can be easily generalised to arbitrary state sequences while keeping the original semantics of temporal operators. 2. The syntax of this OCL extension is quite natural. It introduces usual futureoriented temporal operators such as next, existsNext, always, sometimes as well as their past-oriented duals. We will only use the future-oriented ones because we intend to effectively check properties using the Tina model checker [START_REF] Berthomieu | The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets[END_REF], which does not support past-oriented operators.

Let us go back to our process example to introduce our generalisation. A snapshot of our process has to describe precisely the state of each workdefinition. We take as given a finite set S of such states. Let W D be the set of workdefinitions of the model. Let Σ be the set of the process state: Σ = W D → S.

A trace σ of the process is a maximal finite sequence of process states σ 0 , . . . , σ n , σ i ∈ Σ, where σ 0 denotes the initial process state. Semantically, we have two kinds of transitions. First, continuous time-passing transitions that are here unobservable and consist in incrementing all workdefinition clocks by a quantity dt simultaneously. Second, event-based transitions that change the states of workdefinitions as defined by the expert above. Two consecutive events in a sequence are related through a combination of the time-passing transition followed by an event-based transition.

In order to ease the definition of our properties we introduce the new operator precedes. Such an operator can be described using the previous ones: e 1 precedes e 2 = always!(e 2 ) until e 1 Expressions of our TOCL extension are now OCL expressions over the model elements using these temporal operators. We also allow these expressions to be built over state names defined in the aforementioned set S. The existential ones have to be rewritten in order to be checked: we will verify the negation of each formula. If the analysis gives a correct answer, there is no trace satisfying the property. On the contrary, if the analysis gives a negative answer with a counter-example, the existential property is verified and the counter-example is one of the traces satisfying the temporal property. We only give here the first existential property.

always (not wd.time state = ok) ≡ always (wd.time state = tooEarly ||wd.time state = tooLate)

We have given the textual concrete syntax and the associated semantics of our extension of TOCL. In order to integrate it into a metamodelling approach (i.e. defining properties at the metamodel level), it is necessary to define, at the MOF level, the OCL abstract syntax and its temporal extension. To give the ability for any DSL to use TOCL, we start from the OCL metamodel defined in [START_REF] Richters | A metamodel for OCL[END_REF] and promote it at the MOF level [START_REF]Meta Object Facility (MOF) 2.0 Core Specification[END_REF] (fig. 3). We also add the set of temporal operators defined in [START_REF] Ziemann | An extension of OCL with temporal logic[END_REF] and in the aforementioned extension (fig. 3).

We have now introduced the concrete and abstract syntax and semantics of our temporal OCL extension. With these temporal constraints we are now able to express complex properties on the behaviour of the model to be checked. One immediate application of these constraints is the transformation of every invariant as defined in OCL as the first kind of properties. We now consider executing models and each invariant has to be checked in every process state of all possible traces. Therefore, we rename invariant expressions e to always e.

The next part introduces how these model states can be built using OCL over model attributes.

Denotational Semantics to Petri Net and LTL

In this study, we choose to use the technical space of Petri nets as the target representation for formally expressing our process models. We also choose to express our temporal formulae as LTL formaluae (Linear Temporal Logic) over the Petri net associated to a process model. Then we manipulate Petri nets and LTL formulae within the Tina9 toolkit. TINA (TIme Petri Net Analyser) is a software environment to edit and analyse Petri nets and timed nets [START_REF] Berthomieu | The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets[END_REF]. The different tools constituting the environment can be used alone or together. Some of these tools will be used in this study:

nd (NetDraw) : nd is an editing tool for automatas and timed networks, under a textual or graphical form. It integrates a "step by step" simulator (graphical or textual) for the timed networks and allows to call other tools without leaving the editor. -Tina : this tool builds the state space of a Petri net, timed or not. Tina can perform classical constructs (marking graphs, covering trees) and also allows abstract state space construction, based on partial order techniques. Tina proposes, for timed networks, all quotient graph constructions discussed in [START_REF] Berthomieu | Réseaux de Petri temporels : méthodes d'analyse et vérification avec TINA[END_REF]. -selt: usually, it is necessary to check more specific properties than the ones dedicated to general accessibility alone, such as boundedness, deadlocks, pseudo liveness and liveness already checked by tina. The selt tool is a model-checker for formulae of an extension of temporal logic seltl (State/Event LT L) of [START_REF] Chaki | State/event-based software model checking[END_REF]. In case of non satisfiability, selt is able to build a readable counter-example sequence or in a more compressed form usable by the TINA simulator, in order to execute it step by step.

Denotational Semantics of SIMPLEPDL

PetriNet In this case study, we use timed Petri nets as a paradigm to express the semantics of our processes, models of SIMPLEPDL. The semantics is now a denotational one defined as a mapping from SIMPLEPDL to Petri nets. The Petri nets metamodel is given in Figure 4. A Petri net (PetriNet) is composed of nodes (Node) that denote places (Place) or transitions (Transition). Nodes are linked together by arcs (Arc). Arcs can be normal ones or read-arcs (ArcKind). The attribute tokensNb specifies the number of tokens consumed in the source place or produced in the target one (in case of a read-arc, it is only used to check whether the source place contains at least the specified number of tokens). Petri nets markings are defined by the tokensNb attributes of places.

Finally, a time interval can be expressed on transitions. Mapping The translation schema that transforms a process model into a Petri nets model (SIMPLEPDL2PETRINET) is given in Figure 5. Each workdefinition is translated into four places characterising its state (NotStarted, Started, InProgress or Finished). A WorkSequence becomes a read-arc from one place of the source workdefinition to a transition of the target workdefinition. The state Started records that the workdefinition has been started. We also add five places that will define a local clock. The clock will be in state TooEarly when the workdefinition ends before min time and in the state TooLate when the workdefinition ends after max time.

Our transformation has been written in ATL, ATLAS Transformation Language [START_REF] Jouault | Transforming models with ATL[END_REF]. A first rule expresses one workdefinition in terms of places and transitions. A second one translates a work sequence into a read-arc between the adequate place of the source workdefinition and the appropriate transition of the target workdefinition. Finally a third rule considers the whole process and builds the associated Petri net.

In order to manipulate the obtained Petri net inside a dedicated tool such as Tina, we have composed the preceding transformation with a transformation PETRINET2TINA that translates a PetriNet model into the textual syntax of the Tina tool. ------------------ ------------------ Traceability The set of translation choices (i.e. the mapping) defined in the SIM-PLEPDL2PETRINET transformation is captured in the ATL source code. The benefit of this language is that it is itself defined as a metamodel. It allows to obtain a model (conform to the ATL metamodel) corresponding to the transformation. This transformation model can be reused as an entry model for another transformation (Higher Order Transformation). We can remark that it is possible to enrich traceability information as proposed by [START_REF] Jouault | Loosely Coupled Traceability for ATL[END_REF].

Denotational Semantics of TOCL The transformation model defined during the translation to Petri nets is used to instantiate a generic transformation that defines LTL properties from the initial metamodel properties, instantiated relatively to the initial process model.

Our experiments show a lack in current MDE technology that does not allow to parameterise a model transformation. The use of a programming language such as Java, as well as a specific library such as EMF, is necessary to handle such a transformation.

Models Validation and Feedback

Model checking results have to be interpreted at the SIMPLEPDL model level in order to provide a complete front-end to the end-user. Properties verified in the Petri net correspond to a double instantiation of the properties expressed at the metamodel level. The interpretation of the results must be the conjunction of the results obtained for the different instantiations of a metamodel property.

The feedback of properties results (catching in a first time the truth value of the property) in the model, can be automatically computed using the transformation model defined during the translation SIMPLEPDL2PETRINET. This translation captures the set of choices that have been done during the transformation (i.e. the mapping table). This technique uses a Higher Order Transformation that takes a transformation model and allows to trace back the model checker interpretation into the DSL model.

In a first time, we only handle the boolean value returned by the Tina analyser. When the LTL properties associated to one SIMPLEPDL properties are satisfied, the property is satisfied. In the other case, the transformation model allows to identify in the model the faulty element and to update its dynamic information in order to visualise the state in which the property failed. We have to take care of the kind (universal or existential) of temporal properties expressed. In case of an existential one, the negation of the result has to be returned.

The next step consists in handling counter-examples. Such counter-examples generated by the model checker could be expressed on the model and be then injected in the model animator (e.g. the SIMPLEPDL animator) defined in the Topcased project.

Related Works

Models Semantics

The formal semantics definition of modelling languages is an active research field in the MDE community. Beside our previous works presented in [START_REF] Benoit Combemale | Towards a rigorous metamodeling[END_REF] and [START_REF] Benoit Combemale | Sim-plePDL2Tina : Mise en oeuvre d'une Validation de Modèles de Processus[END_REF], we have identified other projects that consider this important subject.

The ISIS laboratory of the Vanderbilt University focuses on MDE for many years. They proposed the MIC approach (Model-Integrated Computing), in which models are at the heart of the integrated software development. Recently, they propose, in [START_REF] Chen | Semantic anchoring with model transformations[END_REF], a semantics anchored to a model of formal semantics built upon ASM (Abstract State Machine) [START_REF] Gurevich | The abstract state machine paradigm: What is in and what is out[END_REF], using the transformation language GReAT (Graph Rewriting And Transformation language) [START_REF] Agrawal | The design of a language for model transformations[END_REF].

Xactium10 is a company wbose objectives are to provide practical solutions for the development of systems based on MDE principles. It developed the XMF-Mosaic tool [START_REF] Clark | Applied metamodelling -a foundation for language driven development[END_REF] that allows to define a DSL, to simulate and to validate models using a extension of the OCL language named xOCL (eXecutable OCL). XMF-Mosaic also provides means to transform models and to define translations to other technical spaces.

These works are very near to the objectives of the TOPCASED environment, i.e. to propose a modular modelling environment based on a modular generative approach (like GME, XMF), as well as a formal semantics that provides simulation and model validation tools. Our works based on Kermeta follow an approach similar to the ones of xOCL inside the XMF-Mosaic tool.

The semantics anchoring proposed by the ISIS laboratory is similar to the denotational semantics like the mapping to Petri nets we propose. The main difference is that we want to give more flexibility in the choice of the semantics model and to allow easier feedbacks from simulations or verifications inside a particular model. However, they do not propose the use of models rewriting rules to define the operational semantics.

Models Verification

Verification of UML models In order to specify structural properties on UML models, OCL was introduced. It is therefore accepted as the standard language to express structural properties on UML models. There also exists a bunch of tools to check OCL properties for any model.

As for temporal properties, some recent works intend to extend the usual OCL syntax and semantics to give the capability to express temporal constraints. All these works address OCL extensions in an UML context. They do not address how the transition system is derived from the model.

The aforementioned work of [START_REF] Ziemann | An extension of OCL with temporal logic[END_REF] proposed to extend OCL with temporal operators and defined their semantics on the trace semantics of the UML model. This work is a first step towards the simulation of temporal properties over traces using the USE tool.

Some works, such as [START_REF] Flake | Temporal OCL extensions for specification of real-time constraints[END_REF] and [START_REF] Flake | Formal semantics of static and temporal state-oriented OCL constraints[END_REF], are focused on the expression of real time constraints while keeping the original OCL syntax. They relied on StateChart states to express the dynamic constraints of the system. Then, they mapped their constraints into Clocked-CTL.

[6] proposed to express real time constraints using two new classes Time and Events. A new OCL template is introduced and the usual ones (pre-, post-, inv and action) are translated in it. The semantics is also defined as a trace semantics.

In [START_REF] Distefano | Towards model checking OCL[END_REF], the authors expressed non temporal OCL constraints into their objectoriented version of CTL. They defined formally what is a state of the UML model. They are able to check whether a property expressed in OCL can be checked in every reachable state. The work of [START_REF] Bradfield | Enriching OCL using observational mu-calculus[END_REF] introduced new OCL templates. They mapped them into Oµ(OCL)calculus, an observational µ-calculus, which expressions are OCL expressions. The semantics of their Oµ(OCL)-calculus is defined over the states of [START_REF] Distefano | Towards model checking OCL[END_REF]. Using model checking tools, the author intends to check the property on a CCS term modelling their UML system.

All the previous works only specify the way OCL must be extended to deal with temporal formulae in order to verify or simulate them later but do not reach this last step, at least not in an automatic manner. For instance, the point of generating the transition system from the initial UML is not solved.

Verification of DSL models OCL was initially defined on UML but was quickly defined for every metamodel. It is the main tool to express structural properties in DSL. Existing OCL checkers are also model independent.

Conclusion & Future Works

The context of this article was to integrate formal methods for refining DSL semantics. DSL semantics is usually restricted to structural properties and dynamic aspects are often only informally described or are even implicit. As our aim is to express and validate behavioural and operational properties within a metamodelling framework, the first step was to introduce and handle an operational semantics, instantiated in this article to our process metamodel SIMPLEPDL. This semantics is introduced with respect to properties of interest, given by an expert of the domain. First, a notion of state is introduced, followed by the definition of transitions and executions. Temporal operators, forming temporal properties, are also introduced. In order to check these properties, first a denotational semantics is provided as a mapping from SIMPLEPDL processes to Petri nets, second a front end to the Tina model-checker is defined.

Few things still remain to be done. In particular, the current presentation is focused on SIMPLEPDL, it still needs to be abstracted away to get a more general approach. The formal connection between the observational operational semantics and the denotational semantics induced by the ATL transformation have to be validated.

Currently, we are implementing a prototype allowing us to define metaproperties through an Ecore modelling language extension given by the Eclipse EMF plugin. The expression of temporal properties uses an extension of OCL metamodel provided by the EMFT plugin on which we add the set of temporal operators described above, in the article. An interface associated to the TOCL textual concrete syntax will be integrated using generators such as Sintaks [START_REF] Muller | Model-driven analysis and synthesis of concrete syntax[END_REF] or TCS [START_REF] Jouault | TCS: a DSL for the Specification of Textual Concrete Syntaxes in Model Engineering[END_REF]. Our prototype must also integrate the set of ATL transformations and provide a front end to Petri nets using the Tina toolkit, through the SIMPLEPDL language. We still have, in case of a negative answer from the model checker, for a given property, to retrieve the generated counter-example. It can then be injected within both the model animator currently developed with the TOP-CASED project and the SIMPLEPDL model graphical editor defined with TOPCASED.

Fig. 1 :

 1 Fig. 1: SIMPLEPDL metamodel

Fig. 3 :

 3 Fig. 3: Temporal OCL integration to MOF

Fig. 4 :

 4 Fig. 4: Petri Nets Metamodel

Fig. 5 :

 5 Fig. 5: Translation schema from SIMPLEPDL to PetriNet

  Let w be the considered Work Definition. ∀ws = w.predecessor, (ws.linkType = startToStart&&ws.linkToPredecessor.state = started) ||(ws.linkType = f inishedToStart&&ws.linkToPredecessor.state = f inished) notStarted, notFinished, clock → started, notFinished, 0 ∀ws = w.predecessor, (ws.linkType = startToFinished&&ws.linkToPredecessor.state = started) ||(ws.linkType = f inishedToFinished&&ws.linkToPredecessor.state = f inished) started, notFinished, clock < min time → f inished,tooEarly, clock started, notFinished, clock ∈ [min time, max time] → f inished, ok, clock started, notFinished, clock > max time → f inished,tooLate, clock Fig. 2: Event-based Transition Relation for WorkDefinitions

http://www.eclipse.org/emf/

http://www.isis.vanderbilt.edu/projects/gme/

Toolkit In OPen source for Critical Applications and SystEms Development, http://www. topcased.org

We propose an analysis of the SPEM 2.0 standard in[START_REF] Bendraou | Definition of an Executable SPEM2[END_REF]

http://www.eclipse.org/epf/

Open Source Library for OCL, http://oslo-project.berlios.de.

The Eclipse Modeling Framework Technology project, http://www.eclipse.org/emft/

Worst Case Execution Time

http://www.laas.fr/tina/

http://www.xactium.com


Darlam Fabio Bender

Benoît Combemale

Xavier Crégut

Jean Marie Farines

Bernard Berthomieu

François Vernadat

Ladder Metamodeling & PLC Program Validation through Time Petri Nets

Ladder Diagram (LD) is the most used programming language for Programmable Logical Controllers (PLCs). A PLC is a special purpose industrial computer used to automate industrial processes. Bugs in LD programs are very costly and sometimes are even a threat to human safety. We propose a model driven approach for formal verification of LD programs through model-checking. We provide a metamodel for a subset of the LD language. We define a time Petri net (TPN) semantics for LD programs through an ATL model transformation. Finally, we automatically generate behavioral properties over the LD models as LTL formulae which are then checked over the generated TPN using the modelcheckers available in the Tina toolkit. We focus on race condition detection.

Introduction

Actually, verifications of Programmable Logical Controllers (PLCs) programs are made through exhaustive testing. This method takes a long time to be executed and some errors may pass unnoticed in complex systems.

Ladder Diagram (LD) programs are difficult to debug and modify because its graphical representation of switching logic obscures the sequential, state-dependent logic inherent in the program design [START_REF] Guasch | Fault diagnosis for gas turbines based on the control system[END_REF]. Not found bugs in PLC programs are often very costly and sometimes are even a threat to human safety. This work aims to provide a framework for automatic formal verification of PLC programs written in LD language.

To perform the formal verification of LD programs we introduce a model driven approach. LD models are designed according to an LD metamodel. These LD models are then translated into a formal language. The generic LTL properties to be verified are generated automatically, and finally we rely on model-checking to verify the temporal properties. For this work we have chosen the time Petri nets (TPN) as formal language, and the Tina4 toolkit for simulation and model-checking. We focus on the verification of generic, i.e. model independent, properties, especially the absence of race conditions in LD programs.

This paper is organized as follows. Section 2 introduces the PLCs, the LD language and the validation issue. Section 3 presents the approach used to formally verify LD programs. Section 4 presents the related work and Section 5 concludes and presents some perspectives and future work.

2 PLCs, Ladder Diagrams and Validation Issue

Programmable Logical Controllers (PLCs)

A PLC is a special purpose industrial computer used to automate industrial processes. It can be connected to several inputs and outputs, and can be programmed to control the state of the outputs depending on the configuration of the inputs and its internal state.

The PLC execution follows a cycle. The state of all inputs is copied into memory. Then, the internal program runs and creates in memory a temporary table of all outputs. When this program completes, the table is written to the outputs and a new cycle starts. It repeats as long as the PLC is running.

A PLC can be programmed using any of the five languages [START_REF]International Electrotechnical Comission: IEC 61131-3 International Standard, Programmable Controllers, Part 3: Programming Languages[END_REF] which are: Instruction List (IL), Structured Text (ST), Function Blocks Diagrams (FBD), Sequential Function Chart (SFC) and Ladder Diagram (LD). The semantics of these languages is not strictly defined, certain definitions are missing or contain ambiguities. Some research work has been made to solve these ambiguities, e.g. [START_REF] Tourlas | An assessment of the IEC 1131 -3 standard on languages for programmable controllers[END_REF]. This article focuses on the LD language, but the same approach could be used for the other languages.

Ladder Diagram (LD)

Ladder Diagram is the most used language for programming PLCs. It is a graphical language where the basic elements are based on an analogy to physical relay diagrams [START_REF] Schum | Locksmithing and Electronic Security Wiring Diagrams[END_REF], so it does not represent a big paradigm shift for technicians that are not used to the new computer techniques and programming languages. In Figure 1 is represented a simple LD program in the textual concrete syntax (ASCII art) normally used. We can look at it as a relay diagram where the power flows from the left to the right, passing through the inputs to activate the outputs. The program is delimited by a vertical line on the left representing the hot wire, and another one on the right representing the neutral wire. These vertical lines are called the left and right rails.

The horizontal lines (rungs) and the associated elements represent boolean equations. The dependent element of the equation (coil) is represented by the symbol "( )", while the independent elements (contacts) are represented by "| |". A diagonal line is placed in the middle of symbols as in "|/|" to indicate that the negated value of the variable is used. Variables placed in series represent the AND boolean function while The elements presented so far are the basic elements of LD. A program may also contain more complex elements, the functions and function blocks (FB). Functions always produce the same outputs when provided with the same inputs while FBs keep an internal state that also influences the outputs. They are represented by a rectangular box with their names inside, their inputs on the left side, and their outputs on the right side. These boxes are connected in the diagram's rungs through its inputs and outputs. The LD language also provides other imperative elements (procedures, goto) that are not treated in the scope of this work.

It can be noted that LD programs are hard to visualize and become unreadable even for small to medium size programs. The validation of these programs through exhaustive testing are very expensive and unsure. A method for their formal verification is then of great help for system engineers.

Ladder Diagram Validation

In this work we intend to create a framework for automatic verification of temporal properties in LD programs. The properties to be verified over an LD program could be generic (and apply to every model) or specific to one model. Model related properties must be formulated by the programmer, while generic properties only rely on the metamodel concepts and can be automatically generated from the model.

One of the important generic properties to be verified on an LD program is the absence of race conditions [START_REF] Aiken | Detecting races in relay ladder logic programs[END_REF]. A race condition is an undesirable situation that occurs when a device or system attempts to perform two or more operations at the same time but, because of the nature of the device or system, the operations must be done in the proper sequence in order to be done correctly. A race condition occurs in an LD program when under fixed inputs and function block states, one or more outputs keep changing their values. In the LD example of Figure 2, the variable A is an input, C and D are memory, B and E are outputs. It can be seen that even if A is kept stable, the variables C, D and E will not stabilize thus it is an example of race condition. This kind of problem is sometimes difficult to detect with traditional techniques, and bugs not detected during the test period can be very costly to correct later. In section 3.4 we present how to express this property as a LTL formulae and how to automatically generate and validate the formulae from the model.

MDE-Based Approach for Formal LD Program Validation

The approach we chose to verify properties in LD programs consists in translating the semantics of LD programs to a language formally (mathematically) defined. The chosen formal language is the Time Petri Net (TPN) [START_REF] Merlin | Recoverability of communication protocols-implications of a theoretical study[END_REF].

To define and execute the translation we used a model driven engineering (MDE) approach. LD Programs are models that must conform to the LD metamodel. These models are then translated to a TPN model that conforms to a TPN metamodel. This TPN model is then translated to the input format of the Tina tool. General properties over the Ladder model are also automatically generated as LTL formulae. Finally, we use model-checking to verify the properties represented in LTL formulae over the generated TPN. A general schema of the process can be seen in Figure 3. All translations between models cited above were written in ATL (ATLAS Transformation Language) [START_REF] Jouault | Transforming Models with ATL[END_REF]. This language can be used to write translations of type model-to-model (M2M) and modelto-text (M2T). In this case study we have developed one M2M (Ladder2PetriNet) and two M2T (PetriNet2Tina and Properties) transformations.

Ladder Diagram Metamodel

The first contribution of this study is the definition of a metamodel for a subset of the LD language. An incremental approach has been chosen to build the metamodel. As a first step it was built a metamodel able to represent a significant subset of the LD language. This metamodel can be seen in Figure 4. An LD program (Program) is composed of variables (Variable) and rungs (Rung). A variable may represent an input, output or memory location (InOutKind). A rung is composed of elements (Element) that denote basic (BasicElement) and complex (ComplexElement) elements.

A basic element can be "normal_open" or "normal_closed" (PlacementKind). It denotes either a coil (Coil) or a contact (Contact) and always references a Variable. Complex elements represent functions and FBs. The attribute kind contains the name of the represented function or FB (Functions). Complex elements are composed of inputs (Input), outputs (Output) and internal variables (InternalVariable). The enumeration Functions can be easily extended to contain all the standard functions and FBs.

| A B | +--------| |------------------( )-----+ | C D | +--------|/|------------------( )-----+ | D C | +--------| |------------------( )-----+ | C E | +--------| |------------------( )-----+

Fig. 2. Simple example of races in LD

We introduce in this work the concept of path (Path). A rung is composed of paths. A path is a closed circuit by which the power can flow through the contacts to activate a coil. In the example of Figure 1 A path may have any number of contacts or outputs of complex elements as operators (Operator) but only one coil or input of complex elements as result (Result). The restriction of only one result per path was introduced to facilitate the translation later, but it does not introduce loose of generality because a path with n results can always be decomposed into n paths with one result. Note that Result is a generalization of the elements that may have their state changed by the power flow, while Operator is a generalization of the elements that are conditions for the power flow.

The data type of an internal variable of complex elements are restricted in this work to Boolean and Integer (VariableType) and the global variables of the program (Variable) are restricted to Boolean.

Time Petri Nets, SE-LTL and Tina Toolbox

In this study, we have chosen the technical space of time Petri nets as the target representation for formally expressing our LD semantics. We also have chosen to express our temporal properties as LTL formulae (Linear Temporal Logic) over the Petri net associated to a LD model. Then we manipulate Petri nets and LTL formulae within the Tina toolkit. Time Petri Nets Time Petri net (or TPN) [START_REF] Merlin | Recoverability of communication protocols-implications of a theoretical study[END_REF] is one of the most widely used model for the specification and verification of real-time systems. TPNs are Petri nets in which a nonnegative real interval I s (t), with rational end-points, is associated with each transition t of the net [START_REF] Merlin | Recoverability of communication protocols-implications of a theoretical study[END_REF]. Let R + be the set of nonnegative reals. For i ∈ I + , ↓ i denotes its left end-point, and

Tina

↑ i its right end-point (if i bounded) or ∞. For any θ ∈ R + , i - . θ denotes the interval {x -θ|x ∈ i ∧ x ≥ θ}.
States and the temporal state transition relation t@θ -→ are defined as follow:

Definition 2. A state of a TPN is a pair s = (m, I) in which m is a marking and I is a function called the interval function. Function I : T → I + associates a temporal interval with every transition enabled at m. We write (m, I)

t@θ -→ (m ′ , I ′ ) if θ ∈ R + and: 1. m ≥ Pre(t) ∧ θ ≥ ↓ I(t) ∧ (∀k ∈ T )(m ≥ Pre(k) ⇒ θ ≤ ↑ I(k)) 2. m ′ = m -Pre(t) + Post(t) 3. (∀k ∈ T )(m ′ ≥ Pre(k) ⇒ I ′ (k) = if k = qt ∧ m-Pre(t) ≥ Pre(k) then I(k) - . θ else I s (k))
States evolve as follows: assume the current state is s = (m, I), t is enabled at m, and became last enabled at time τ. Then t cannot fire before time τ + Min(I(t)), and must fire no later than τ + Max(I(t)), except if firing another transition before t made t not enabled anymore. Firing transitions takes no time.

TPN Metamodel

The time Petri nets metamodel is given in Figure 6. A Petri net (PetriNet) is composed of nodes (Node) that denote places (Place) or transitions (Transition). Nodes are linked together by arcs (Arc). Arcs can be normal ones or read-arcs (ArcKind). The attribute weight specifies the number of tokens consumed in the source place or produced in the target one (in case of a read-arc, it is only used to check whether the source place contains at least the specified number of tokens). Petri nets marking is defined by the tokens attribute of Place. Finally, a time interval can be expressed on transitions. Formulae Φ of State/Event -LT L are defined according to the following grammar:

Φ ::= p | a | ¬Φ | Φ ∨ Φ | Φ | Φ | ♦ Φ | Φ U Φ Example of State/Event -LT L formulae :
(For all paths) P P holds at the beginning of the path, P P holds at the next step, P P globally holds, ♦ P P holds in a future step, P U Q P holds until a step is reached where Q holds Tina Toolbox for Time Petri Nets Verification Tina (TIme Petri Net Analyzer) is a software environment to edit and analyze Petri nets and time Petri nets [START_REF] Berthomieu | The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets[END_REF]. The different tools constituting the environment can be used alone or together. Some of these tools will be used in this study:

nd (Net Draw) : nd is an editing tool for automata and TPN, under a textual or graphical form. It integrates a "step by step" simulator (graphical or textual) for the TPN and allows to call other tools without leaving the editor. tina : this tool builds the state space of a Petri net, timed or not. It can perform classical constructs (marking graphs, covering trees) and also allows abstract state space construction, based on partial order techniques. It proposes, for TPN, all quotient graph constructions discussed in [START_REF] Berthomieu | Time petri nets analysis with tina[END_REF]. selt: usually, it is necessary to check more specific properties than the ones dedicated to general accessibility alone, such as boundedness, deadlocks, pseudo liveness and liveness already checked by tina. The selt tool is a model-checker for an enriched version of State/Event -LT L. In case of non satisfiability, selt is able to build a readable counter-example sequence or in a more compressed form usable by the Tina simulator, in order to execute it step by step. The selt logic is rich enough to encode marking invariants like (p1 + p3 >= 3).

Example of selt formulae :

t1 ∧ p2 ≥ 2
for every path t1 and m 0 (p2) ≥ 2, (p2 + p4 + p5 = 2) a linear invariant marking, (p2 * p4 * p5 = 0) a non linear invariant marking, selt also allows to define new operators : in f ix q R p = (p ⇒ ♦ q) definition of a "Responds to" operator, (denoted R), t1 R t5 t1 "Responds to" t5.

Translational Semantics of LD Programs through Time Petri Nets

In order to apply the model-checking techniques to verify an LD program using the available tools, it is necessary to represent the semantics of the program in a formal language. In this section we describe the translational semantics of an LD program in the form of a TPN. The semantic transformation is based on the metamodel of the LD language (Figure 4) and the metamodel of the TPN (Figure 6). It was coded using ATL [START_REF] Jouault | Transforming Models with ATL[END_REF]. In this first work we do not translate the complex elements of the LD language, note that the complex elements represent the functions and FB of the LD language, these elements have a unique semantics so a complete translation would have to take into account the specific semantics of each function or FB.

The ATL code is composed of eight matched rules. A matched rule enables to match some of the model elements of a source model, and to generate a number of distinct target model elements. Figure 7 shows what target elements are created for each rules. We use rule inheritance to filter different elements that are represented by a unique class in the metamodel. This inheritance could had been done at the metamodel level but our approach allows to keep the metamodel at a higher abstraction level and also allows to factorize the ATL code.

Each LD Program will be translated to a TPN. This TPN can be divided in three different groups of elements (Figure 8), each one with a different purpose during the simulation.

The first group is responsible for controlling the execution according to the PLC operation, a place is introduced for each execution step, that is, read the inputs, execute all the ordered rungs one by one, then update the outputs. The transitions are timed " [START_REF] Guasch | Fault diagnosis for gas turbines based on the control system[END_REF][START_REF] Guasch | Fault diagnosis for gas turbines based on the control system[END_REF]" so as to guarantee that all the actions depending on one execution step (these actions are timed "[0, 0]") are executed before the state is changed. This mechanism is used to give a higher priority to transitions associated with the second and third group. We could have achieved the same effect by using prioritized Petri nets (PrTPNs) [START_REF] Berthomieu | Model-checking bounded prioritrized time petri nets[END_REF].

The second group represents the value of the variables. Each variable contained in the program will be translated into two places, one representing the False (Variable-Name_0) and the other the True (VariableName_1) state of the variable. Transitions are also created to set and reset these variables. Note that transitions of this group -describing the behavior of the environment -evolve in parallel and remain active between the capture of the environment (transition input_reading) and its update (transition re-set_variables). This simplified modeling of the environment will result in a very strong combinatorial explosion.

The third group represents the execution semantics. This group is composed of two places for each variable as in the second group, but in this case the variables do not represent the real value of the variable, but are used to calculate the new values. This group represents the simulation variables. Input variables will have their simulation value copied from the real value -on the second group -during the input reading state. Output variables are calculated during the execution of the rungs and at the end, during the output update state, the real value -on the second group -will be updated according to the result of computation. At the end of each cycle all simulation variables are reset. Figure 7 represents the elements generated for each of the eight rules. In some cases, elements generated by one rule are used by another rule. For example, the place input_reading is created by the rule Program2PetriNet and then is used by the rule Input2PetriNet.

The translation of paths generates the elements that calculate the value of the outputs according to the inputs. In Figure 7 (Path2PetriNet) one can see the elements generated by applying this rule to the first path of Figure 1. This path represents the boolean equation C = A ∧ ¬B.

The translation method generates a safe (1-bounded) TPN. This is guaranteed by the transformation. A structural analysis of the TPNs generated by the translation gives one invariant for all places in the first group, and one invariant for each couple of places representing the state True or False of variables.

Formal Verification of Race Conditions in LD Programs

In this section we demonstrate how to express the properties we wish to verify as LTL formulae, how to automatically generate these properties from the LD model and finally how to perform the model-checking with the selt tool.

Formalizing Race Conditions as LTL Formulae

To verify the absence of race conditions in an LD program we need to formally describe this property. We first describe the concept of stability of inputs and outputs. A boolean variable is said to be stable if it does not change its state, that is, it is always True or always False. When we translate an LD program, every boolean variable is represented by two complementary TPN places, (VariableName)_0 representing the false state and (VariableName)_1 representing the true state. Based on that we can formulate the Definition 3.

Definition 3. An LD variable called x is stable if (( x_0) ∨ ( x_1)).
An LD program is free of race conditions if when the inputs are kept stable, all outputs and memory variables will stabilize. This property is represented in Definition 4.

Definition 4. An LD program is free of race condition if

(stable_inputs ⇒ ♦ stable_out puts) where stable_inputs represents a logical AND between the stability condition for every input variable, while stable_outputs represents a logical AND between the stability condition for every output and memory variable.

To reduce the model-checking effort we can decompose the LTL formula into more simple ones. The decomposition is based on the following properties:

♦(( P) ∧ ( Q)) ≡ ♦ P ∧ ♦ Q P ⇒ (Q ∧ R) ≡ (P ⇒ Q) ∧ (P ⇒ R)
Our general property can be decomposed in several different properties, one for each output or memory variable. Then we can check separately if every output will stabilize when the inputs are kept stable. When this property does not hold for a variable x, the LD program has a race on x.

The LTL formula can be simplified even more by applying the cone of influence (COI) reduction. The COI reduction is a technique that reduces the size of a model if the propositional formula in the specification does not depend on all state variables in the structure [START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF]. The COI of a variable x is all the variables that influence the value of x. On the LD program represented in Figure 2 the COI of the variable B is {A}, while the COI of variable C is {C, D}. So we can redefine the Definition 4 as: Definition 5. An LD program is free of race condition if for every output or memory variable V the following property holds:

(COI(V )_stable ⇒ ♦ V _stable), where COI(V )_stable represents the stability condition for every variable in the COI of V .

Automatic Generation of LTL Properties An ATL query was developed to automatically generate the LTL properties in a text format. This query is a M2T transformation that was built over the LD metamodel. It takes as input the LD model and generates the file properties.ltl. The COI of a variable is calculated through iterative searching in the model. We can use the genererated file to verify temporal properties with the selt tool.

Model-checking To perform the model-checking we first use the tina tool to build the state space of the TPN generated by the translation. The selt tool is then used to verify the LTL properties over this state space.

Results

This method was applied to the LD program in Figure 1 and as expected the property was evaluated to TRUE. The program is indeed free of race conditions. When applied to the program in Figure 2 the property was evaluated to TRUE for variable B, and to FALSE for variables C, D and E, proving that this program has a race on these three variables. In Table 1 is presented the size of the TPN and state space generated for both programs.

The results obtained for the two examples prove that the MDE approach can be used for verification of LD programs, transformation may be run on middle to complex LD diagrams. However, this first approach for translation of LD diagrams to Petri Nets can be largely optimised. The use of temporal constraints to simulate the priorities (instead of inhibitor arcs or directly of priorities 5 ) results in an important extra cost. Likewise, the modeling of the environment is very simple (the environment continues to evolve in parallel between two captures) inducing a useless combinatorial explosion. With this translation, the Petri net associated with a LD program able to control a system containing 6 actuators (outputs) and 7 sensors (inputs) generates a state space of 7 million states. The "covering step graph" [START_REF] Vernadat | Covering step graph[END_REF] construction of Tina, exploiting "partial order techniques" [START_REF] Godefroid | Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem[END_REF], allows to reduce drastically this explosion and leads to a state space of 40 states. However, a finer modeling of the environment will have to be carried out to take into account significant LD programs.

Related Works

Numerous authors have been working in formal verification of PLC programs. These works are normally based in two different approaches.

The first approach consists in implementing PLC programs directly in a formal language, and then automatically generate the PLC code. [START_REF] Jimenez | Synthesis of ladder diagrams from petri nets controller models[END_REF] introduces a program based on a set of rules to translate TIPN (Time Interpreted Petri Nets) control specifications into Ladder Diagrams. In [START_REF] Minas | Visual plc-programming using signal interpreted petri nets[END_REF], [17] and [START_REF] Frey | Design and formal Analysis of Petri Net based Logic Control Algorithms (Dissertation[END_REF] a set of tools was presented for implementation of PLC programs using SIPN (Signal Interpreted Petri Nets), symbolic model-checking was used for validation and verification and the control specification was finally implemented through IL. [START_REF] Dierks | PLC-automata: a new class of implementable real-time automata[END_REF] introduces a formalism based on timed state machines called PLC-automata and a translation of this formalism into ST code.

The second approach consists in translating the existing PLC programs into a formal language and automatically perform the verification. This approach permits the use of formal languages for the verification of PLC programs without changing the programming paradigm. Our work is based in this second approach. Some works using this approach have been developed. [START_REF] Heiner | Instruction list verification using a petri net semantics[END_REF] and [START_REF] Heiner | A petri net semantics for the plc language instruction list[END_REF] provide a Petri Nets semantics for a subset of the IL language. [START_REF] Canet | Towards the automatic verification of plc programs written in instruction list[END_REF] provides a framework for automatic verification of programs written in IL, a formal semantics (transition system) is presented for a subset of the IL language, which is directly coded into a model-checking tool (Cadence SMV6 ). It is then possible to automatically verify behavioral properties written in LTL. In [23] LD programs are formally represented through a transition system. In [START_REF] Aiken | Detecting races in relay ladder logic programs[END_REF] a combination of probabilistic testing and program analysis has been used to detect race conditions in relay ladder programs. [START_REF] Rausch | Transformations between different model forms in discrete event systems[END_REF] generally discusses the transformations between NCES (Net Condition Event Systems) State Charts and PLC languages. In [25] is presented a method for formal verification of LD programs through a translation to timed automata. They check model related properties, while we focus on generic properties. The original program is abstracted according to these properties before the generation of the timed automata, in this way, for each property to be verified it may be generated a different timed automata. In [START_REF] Huuck | Software Verification for Programmable Logic Controllers[END_REF] is discussed semantic issues and a verification approach for SFC and IL programs. It uses a model-checking framework to verify SFC programs and it suggests static analysis techniques, a combination of data flow analysis and abstract interpretation to verify IL programs.

Our work is based on this second approach and is the first to present an MDE approach for PLCs program validation.

Conclusion and Future Work

We have introduced in this article a model driven approach for formal verification of LD programs. We have defined a metamodel for a subset of the LD language. LD models are designed according to this metamodel. An LD model is then translated into a formal language (TPN) in the input format of Tina toolkit by means of two ATL transformations. The LTL properties to be verified are generated automatically from the model. Finally we utilize model-checking to verify the temporal properties over the generated TPN.

Some things still remain to be done, the metamodel must be completed to represent the complete LD language. The modelling of LD program s must be refined (specially the modeling of the environment) to reduce the combinatorial explosion.

In order to implement a complete translation of the LD concepts, we need a language directly supporting data processing like Fiacre [START_REF] Berthomieu | FIACRE: an intermediate language for model verification in the TOPCASED environment[END_REF]. Fiacre was designed in the framework of the TOPCASED project [START_REF] Vernadat | The TOPCASED Project -A Toolkit in OPen-source for Critical Applications and Sys-tEm Development[END_REF] dealing with model-driven engineering and gathering numerous partners, from both industry and academics. Therefore, Fiacre is designed both as the target language of model transformation engines from various models such as SDL, UML, AADL, and as the source language of compilers into the targeted verification toolboxes, namely CADP and Tina.

Model related properties must be formulated by the programmer, as LD programmers are not specialists in formal verification, a mechanism must be used to generate the LTL properties from the user specification. One of these mechanisms is presented in [START_REF] Combemale | A Property-Driven Approach to Formal Verification of Process Models[END_REF] where is presented an approach for generating LTL properties from TOCL ones, a temporal extension of OCL. In [START_REF] Nikora | Developing formal correctness properties from natural language requirements[END_REF] is presented a framework for generating formal correctness properties from natural language requirements. The return of the modelchecking counter-examples to the user must be implemented in order to hide to the user the complexities of the target language.

We are currently working on the recognition of the textual concrete syntax (ASCII art) specified in the IEC 61131-3 standard. We want to be able to generate LD models from its textual syntax. The metamodel presented in this article tries to represent the LD language in a format closer to its semantics. For the recognition of the textual syntax we should create an intermediate metamodel that is closer to this syntax and then apply a model transformation to obtain our original model. We are studying the possible solutions, one is the use of TCS [START_REF] Jouault | TCS: a DSL for the Specification of Textual Concrete Syntaxes in Model Engineering[END_REF], that relates metamodel concepts with the textual concrete syntax and allows to build a model from the textual syntax (injector) and also to generate concrete syntax fromo a model (extractor).

Our work demonstrates that it is possible to apply a model driven approach in formal verification of PLC programs. The combinatorial state explosion is a recurrent problem in the formal verification community and several works have been developed to overcome this problem.

Fig. 1 .

 1 Fig. 1. Simple Ladder Diagram example

  we have two paths in the first rung, one representing the boolean equation C = A ∧ ¬B and the other representing the equation C = C ∧ ¬B. Note that this is a simple decomposition of the original equation. We have a single path in the second rung representing the equation D = C.

Fig. 3 .

 3 Fig. 3. General overview of the LD validation approach

Fig. 4 .

 4 Fig. 4. A simplified LD Metamodel

Fig. 5 .

 5 Fig. 5. A Time Petri net

Fig. 6 .

 6 Fig. 6. Time Petri net Metamodel

Fig. 7 .

 7 Fig. 7. Schema of the ATL transformation Ladder2PetriNet

Fig. 8 .

 8 Fig. 8. TPN generated from the LD model on Figure 1

Table 1 .

 1 Size of the TPN and state space generated

	Program	TPN Generated	State Space
	Figure 1 23 places, 24 transitions 462 places, 1432 transitions
	Figure 2 31 places, 31 transitions 486 places, 1094 transitions

This work is supported by the TOPCASED project, part of the french cluster Aerospace Valley (granted by the french DGE), cf. http://www.topcased.org

http://www.laas.fr/tina/

Since March 2008, Tina 2.9.0 supports the priorities.

http://www.kenmcmil.com/smv.html