Arnaud Dieumegard

Marc Pantel

Guillaume Babin

Martin Carton

Tool Paper: A Lightweight Formal Encoding of a Constraint Language for DSMLs

Domain Specific Modeling Languages (dsmls) plays a key role in the development of Safety Critical Systems to model system requirements and implementation. They often need to integrate property and query sub-languages. As a standardized modeling language, ocl can play a key role in their definition as they can rely both on its concepts and textual syntax which are well known in the Model Driven Engineering community. For example, most dsmls are defined using mof for their abstract syntax and ocl for their static semantics as a metamodeling dsml. OCLinEcore in the Eclipse platform is an example of such a metamodeling dsml integrating ocl as a language component in order to benefit from its property and query facilities. dsmls for Safety Critical Systems usually provide formal model verification activities for checking models completeness or consistency, and implementation correctness with respect to requirements. This contribution describes a framework to ease the definition of such formal verification tools by relying on a common translation from a subset of ocl to the Why3 verification toolset. This subset was selected to ease efficient automated verification. This framework is illustrated using a block specification language for data flow languages where a subset of ocl is used as a component language.

Introduction

Domain Specific Modeling Languages (dsmls) are used in many domains where their capabilities were shown to be very useful for assistance in system and software engineering activities like requirements analysis, design, automated generation, validation or verification. The critical system and software industry is one of the domains where they have been used for many years. This has allowed to achieve better quality and safety of the products without having their development cost following exponentially the curve of the systems complexity.

Beside the obvious advantages of relying on dsml's for the formalization of requirements and design elements, and the automation or simplification of these activities, it remains difficult to convince at the certification level on their correctness. Formal methods have been used in this purpose and as such have been proven as being formidable allies, especially for the verification and validation tasks. In the recent upgrade to level C of aeronautics standards DO-178, both technologies were introduced as DO-331 for Model Driven Engineering and DO-333 for Formal Methods. Both documents advocate dsmls use but their combined use given in DO-333 looks more promising that the lone use of dsmls in DO-331. Both documents advocate a precise, complete and non-ambiguous specification of dsmls.

Their specification usually relies first on the model based definition of their concepts using a dsml such as the omg Meta Object Facility (mof). These metamodels are usually completed with static semantics expressed with constraint languages such as the omg Object Constraint Language (ocl) that provides first order logic and model navigation construct. It allows specifying the static properties of the dsml itself and its concepts. Many formal specifications of both mof and ocl have been conducted to assess their properties, validate the standards and participate in the verification of their implementation. These specifications may also provide formal verification tools for models expressed with these languages. However, this was usually not their main purpose and thus these tools do not usually behave well on the scalability side. This contribution targets a more scalable verification dedicated encoding of a subset of ocl in the Why3 verification toolset that can be reused in different dsmls. These dsmls rely on this subset of ocl as a component language. One key change is that the data part of ocl must be adapted to fit the host language.

The Why and WhyML languages are two complementary languages used for formal software verification. The first one is a high level specification language and the second one a powerful programming language (WhyML). In this setting, programs written using the latter are relying on the formal definitions for types, theories and functions prototypes defined with the former. The Why3 toolset provides a harness for the manipulation of both specifications and programs and also for their translation in order to be verified either automatically using smt solvers or manually using proof assistants like Coq, PVS or Isabelle. The Why3 toolset is very powerful in the sense that it allows to benefit from the combined strengths of each managed smt solver and if necessary to rely on manual verification for proofs that may be too difficult to achieve automatically.

By providing a formalisation of a subset of the ocl in the Why3 toolset, we target to build a framework allowing to ease the formal verification of dsmls implementations and instances. In order to do so, we propose a formal specification and implementation of a lightweight version of the ocl language. dsmls specification, expressed using for example mof compliant metamodels and ocl constraints, or their instances can then be translated to the Why language and be automatically and formally verified. Such verification can ensure the correctness of the dsml specification, assess the conformance of its instances, or verify complex properties on the instances. We have applied this approach for the verification of correctness properties over the instances of a data flow languages specification dsml [START_REF] Dieumegard | A software product line approach for semantic specification of block libraries in dataflow languages[END_REF].

This contribution first pictures our use case and its verification in Section 2. We then provide in Section 3 our lightweight formal encoding of the selected subset of ocl using the Why and WhyML languages. We refer to it as lightweight as it does not covers the whole ocl in order to have a better verification automation and scalability. We will additionally discuss the coverage of the ocl specification. We compare our approach to already existing ones in Section 4. We finally conclude and detail some of our perspectives in Section 5.

OCL as a DSML Component

As an Object Constraint Language, ocl has been mainly used to define properties to be verified on class instances in uml. It thus includes first order logic and query facilities over class instances and its data part is strongly related to the uml one. In the omg mda proposal, dsmls were first defined as simplified class diagrams in the mof subset of uml. ocl has then been used to model the static semantics of the dsml elements. Nowadays, most omg standards rely both on mof and ocl as specification languages.

These ones are thus now widely known in the software engineering domain. They can then be used as a language component to be included directly in the dsml [START_REF] Heidenreich | Integrating OCL and textual modelling languages[END_REF] to allow the dsml user to model constraints and queries with a well known and standard notation. omg already enforces the reuse of its languages like ocl in the qvt standard. Other dsmls have integrated ocl as a language component like the use of tocl for the specification of common behavioral requirements for emf dsml models in [START_REF] Zalila | Formal verification integration approach for DSML[END_REF] or for execution trace matching in the feverel dsml [START_REF] Zalila | Leveraging formal verification tools for DSML users: A process modeling case study[END_REF], the Event Constraint Language (ecl) which allows to derive ccsl constraints from emf dsml models [START_REF] Deantoni | ECL: the Event Constraint Language, an Extension of OCL with Events[END_REF], the Behavioral Coordination Operator Language which allows to specify executable model coordination operators [START_REF] Laasch | A functional object database language[END_REF]. These dsmls metamodels combine several metamodel components including the ocl one that relies on identifier to connect to the elements in the other metamodel components. In the usual integration of ocl in uml or mof, the ocl expressions are written in contexts that provides the identifiers from the uml/mof part of the dsml and the data part of ocl is mapped to their data parts. The identifiers can then be used in the ocl expressions like the names of classes, attributes, methods and parameters. ocl itself can define identifiers that bind stronger than the ones from the context. A similar approach is used to connect ocl with other parts in the dsml metamodel. One key point is to connect also the ocl data part with the dsml one.

General approach for the verification of DSMLs

Formalisation of a dsml in order to conduct formal verification activities starts with the formalisation of the dsml structural elements and their properties. It is usually achieved by expressing the dsml structure, and its static semantics (the metamodel and its ocl constraints) with the formalism targeted for the verification. Two approaches are commonly used in that purpose: on the one hand, modeling the dsml in the formal verification platform including the model creation facilities and then building and verifying models directly in such a platform (a kind of denotational semantics); and on the other hand, providing a transformation from the dsml to the verification platform that is applied on each model for verification (a kind of translational semantics). The first one builds the formal model at the language level, whereas the second one works at the instance level. In both cases, the writing (either being manual or automated) of the formal representation is parametrized by the dsml data specification (i.e. the data that are expressed in the models and verified by the constraints).

If the dsml relies on an additional language such as ocl as a component to express properties, it is then also required to translate those properties into the verification formalism. This work can be leveraged by first providing a formalisation for the ocl component language and then relying on this formalisation for the automatic translation of the other parts of the dsml.

Many dsml also include a definition for their execution semantics. This definition can be directly embedded in the dsml definition [START_REF] Benoit Combemale | A Design Pattern to Build Executable DSMLs and associated V&V tools[END_REF]; it can also be defined externally or can be provided using third party component action languages such as alf 1 . The execution semantics should also be expressed using the verification formalism and the associated formal verification platform. This provides an execution semantics formal specification. This one can be manually or automatically translated into the formal verification platform.

Finally, the verification of a dsml is based on the expression of properties to be verified. These properties are either written directly using the verification formalism or automatically generated from the dsml instances. The second approach is preferred as it increase the efficiency of the verification and also eases the verification for the dsml user.

In the following, we illustrate the verification of a dsml through the example of the verification of the BlockLibrary dsml. This dsml allows using a limited subset of ocl as a component language. BlockLibrary dsml instances are translated as Why3 theories. ocl expressions are translated to Why3 expressions relying on the pre-existing formalisation of the restricted version of the language. Finally, high level properties are automatically generated from the dsml instances as Why3 goals to be discharged through the Why toolset.

The BlockLibrary DSML structural specification

The BlockLibrary dsml [START_REF] Dieumegard | Model-based formal specification of a DSL library for a qualified code generator[END_REF][START_REF] Dieumegard | A software product line approach for semantic specification of block libraries in dataflow languages[END_REF] aims at the specification of the structure and semantics of data flow atomic blocks such as the ones at the core of the Simulink or Scade languages. This dsml allows to specify the inherent variability of these blocks structure and semantics. The structural specification part of the dsml is inspired from the concepts of software product lines combined with the object oriented concept of inheritance in order to handle the highly variable nature of the blocks specification. Data types can be attached to blocks specification components (inputs, outputs, parameters and memories). The components are specified with constraints describing their allowed values (specified using a subset of ocl). The semantics of the blocks is expressed with a simple action language that relies on the same subset of ocl to express pre/post-conditions, variants and invariants.

The two main concerns in the dsml are the use of ocl as a language component for the specification of the dsml data and action constraints and the variability management that allows combining parts of the blocks specification into multiple block configurations.

Verification of BlockLibrary instances with Why3

A significant part of the effort in this case study has been focused on the formalisation of the dsml constructs as Why theories to conduct formal proofs of the model completeness, consistency and correctness using the Why3 platform.

A block specification using the BlockLibrary dsml We provide in Figure 1 a simplified specification for the Delay block written using the BlockLibrary dsml. The Delay block outputs the value provided as its first input and delays its value by a certain number of clock ticks. The number of clock ticks is either provided as a parameter of the block or as an additional input. The values of the output of the block for the first clock ticks cannot be computed from the inputs of the block and should thus be provided as either a parameter or as an additional input of the block. The block allows for scalar, vectors and matrix values. The specification provided here is limited to the handling of scalar values and the initial condition can only be provided as a parameter of the block.

A block specification is contained in a blocktype element bundled in a Library construct. The data types used in the specification are declared in the Library. The variant constructs contains the specification for a block structural elements: input (in) and output (out) ports, parameters and memories. For each declaration of a structural element, it is possible to specify its default value and some additional constraints using our subset of the ocl language. We provide such a constraint in line 20, where we specify that the Delay parameter can only have a positive value.

Each variant can extend, in an object oriented way, other variant constructs by relying on the extends construct. This composition is done through two n-ary operators that can be applied on variant constructs: allof and oneof. The former specifies mandatory compositions whereas the former specify alternative compositions. These operators are inspired from the software product line approach for the specification of features hierarchies.

The mode constructs allows for the specification of the blocks semantics variation points. They thus provide an implementation for one or more variant constructs. The previously presented composition language can be used in this purpose. Each mode construct must provide a definition for the compute semantics of the block variation point (lines 57 to 61). It may also provide the optional semantics for the init and update computation phases for the specified block. The blocks semantics are provided using a custom simple action language: the BlockLibrary action language (bal). A mode and its implemented variant make a set of block configurations. This set is extracted from the composition of variant elements through the allof and oneof constructs. The lack of space prevents us to detail further this dsml and we refer the reader to our papers [START_REF] Dieumegard | Model-based formal specification of a DSL library for a qualified code generator[END_REF][START_REF] Dieumegard | A software product line approach for semantic specification of block libraries in dataflow languages[END_REF], the related thesis work2 , and the website3 for additional informations.

BlockLibrary specification verification A transformation translates Block-Library instances to Why theories; ocl-like constraints to predicates relying on a lightweight formalisation of the subset of ocl detailed in Section 3; and semantics specification (specified using the action language) to WhyML functions.

In addition to this translation of the BlockLibrary specification, properties are generated to assess: the completeness (are all possible configurations of a block given in the specification ?) and the disjointness (are all possible configurations of a block expressed only once in the specification ?) of all the Block-Library dsml block specifications. The verification of these two properties is done automatically by smt solvers in a few tenth of a second for rather simple blocks specification to up to a few seconds for mode complex ones containing up to a thousand different configurations for a block.

The most important lesson learned from this experiment was that as soon as the dsml constructs, their attached constraints, and the ocl component expressions are translated to Why, it is straightforward to write or generate high level properties to be verified using the Why and WhyML languages.

The following section summarizes the Why model of the specific subset of the ocl that was necessary for our dsml use case where a subset of the ocl is used as a dsml component.

OCL Formalisation Using the Why Toolset

ocl is a formal language for querying model elements and expressing model properties. It relies on first order logic and model traversal operators. It is guaranteed to be side-effect free and as such cannot modify the model it is applied to. The Why language is more expressive than ocl and can thus be used to encode any ocl construct.

We provide here some details on our formal specification of our specific subset of ocl in Why. It is important to keep in mind that the main objective of the BlockLibrary dsml is to allow for the formal specification of blocks. As such, we enforce the block specifier to provide strictly typed elements. The consequences of this limitation is impacting the subset of the ocl to be handled. It is indeed not required to handle type manipulation operations such as oclIsKindOf or oclAsType among others.

We will go through the support for some of the ocl constructs; the limitations we selected; and the translation strategies in order to go from ocl constructs to Why constructs. As we will not provide the complete details about our translation, we invite the interested reader to refer to our website4 for additional informations.

OCL standard data types and collections

ocl is built on a simple set of types called primitive data types. The Why3 standard library provides a formalisation for primitive data types that largely covers the needs for the mapping of the ocl ones.

ocl primitive values can be gathered in collections that differs regarding their ability to handle multiple occurrences of the same value (Bag, Sequence) or not (Set, OrderedSet) and if these values are ordered (Sequence, OrderedSet) or not (Bag, Set).

In the Why standard library, collections can be modeled as lists allowing multiple occurrences of the same unordered value. This makes them a direct translation for Bag collections. The standard library also provides the support for Arrays that would directly map to the Sequence collection and Sets for Set collection in ocl.

In our implementation of ocl, we do not take into account the type of the collections and only provide support for Bag collections as lists. This allows to simplify their management in our implementation as it removes the side effects on the collection management operations such as that elements are not automatically removed from the collections as multiple occurrences are allowed. We defined a Why theory called OCLCollectionOperation containing the definition for some basic list accessors and operations. The other three kinds of ocl collections will be implemented in a similar way in a near future with no specific issues expected.

We decided not to support messaging related constructs and tuples constructs. Messaging is related to uml sequence and state machine diagrams which was out of the scope of our case study. Tuples are also missing in our implementation and could be implemented on a first approximation by relying on record types in Why.

OCL operations translation strategy

ocl defines multiple operations that are to be applied either on primitive valuesreferred to as standard language operations -or on collection values -referred to as collection and iteration operations. Some of these operations are not supposed to be used on Bag collections and explicit conversions between collections types must be done. We do not enforce this currently in our implementation of ocl as we provide only one type of collection.

The translation of ocl expressions to the Why language can be done using two strategies. First, operations can be translated to basic first order logic expressions and thus can directly be used in Why. Second, the definition for the operations can be axiomatized using Why function declarations and ocl constraints are translated as expressions using these functions. In our work, we rely on a combination of the two. The list getter is used for simple collection accesses, standard type operations have been defined as functions in Why, simple collections operations are directly mapped to their logical expression equivalent.

This approach has the advantages of easing the translation work as the semantics of ocl standard types operations is already defined and thus avoid to generate too complex expressions. This has the pleasant side effect of easing the transformation verification activities as the translation itself is simpler.

In the following, we provide the mapping between the source ocl constructs and operations and the target Why predicates, functions and expressions.

OCL standard library operations

In ocl expressions, operations can be applied on primitive ocl types. These operations are classical handling of primitive data types and are gathered in the ocl standard library. They have already been formalized in the Why library. We thus rely on their formalisation for our translation.

We did not currently implement the transformation for the div and mod operations on ocl Double elements. The div operation is of particular interest as its behavior in ocl and in Why are not the same. Indeed where the ocl implementation of div applied to any number and 0 (division by zero) returns the null value, the Why version is simply not defined and rejected by the formal verification toolset. The management of specific values like null and invalid is not done and is a chosen limitation of our work to simplify the formal models and reduce the verification costs by avoiding three value logics (True, False and invalid ). We give later more details regarding the related restrictions.

Boolean ocl expressions are implemented using boolean expressions in Why. xor operator has been implemented with and, or and not operators. Numeric operations have been implemented using the standard Why arithmetic theories and their operators. Finally relational operators are also based on standard Why constructs.

Collection operations

As previously mentioned, there are four types of ocl collections. We only considered the use of the bag collections in our case study. In our handling of ocl collection operations, we do not handle ocl generic nature nor subtyping of elements. If the same operation is to be expressed on different types, it is then developed separately for each different type. Whereas this may seem to be a limited way of handling this problem, in practice, our supported restriction of ocl makes this easier as only a few operations needs to be encoded several times. Both kind of polymorphism could be handled by synthesizing sum types representing the allowed set of types for an operation and appropriate pattern matching that mimics late binding at a higher verification cost.

Our partial handling of ocl collections has an impact on the translation provided for some collection operations. The append and including operations have the same implementations and so are subOrderedSet and subSequence. According to the ocl specification, some collections operations are not allowed on bag collections: append, at, first, indexOf, indexAt, last, prepend, subOrderedSet, subSequence. We decided to allow their use in our implementation of ocl. This is a significant drift from the ocl standard but it has the advantage of greatly simplifying the translation mechanism without restraining the expressiveness of the language. This restriction could be enforced easily at the static semantics level. The formalisation of the usual ocl collections is of additional complexity as studied by Mentré et Al [START_REF] Mentré | Discharging proof obligations from Atelier B using multiple automated provers[END_REF] but was not of primary interest for our current work so we decided not to address the related issues.

Each of these functions are defined through a set of axioms specifying their context of use: on which element type they are defined; what restrictions are required for their definitions; and the result of their computation according to the provided input values. The restrictions on their parameters are used to avoid the invalid value. The effort needed in order to achieve the complete verification remains important but is highly lightened by the use of smt solvers to automate the verification.

Logical property assessment iteration operations

Iteration operations are the main operations used on ocl collections. They allow to assess a logical property verification on: every element of a list (forAll), at least one element of a list (exists), exactly one element of a list (one). They can also express the uniqueness of the result of the application of a function on every element of a list (isUnique). All these operations returns a boolean value.

In Table 1, we provide the translation for the forAll, exists, one and isUnique ocl operations on collections. Unlike the previous translations, we do not rely on predefined functions but we rather map these operations to simple first order logic expressions. Regarding the translation of the condition expression: exp, the defined ocl iterators: it, it1 and it2 are mapped to a call to the position of the element in the collection via the list getter operator. In practice, references to it or it1 are replaced by a[i] and references to it2 are replaced by a[j] in exp. This is expressed using the function application: [a/b]c that substitute a to b in c.

ocl expression

Target Why code a→forAll(it: DT | exp)

∀ i: int. 0 ≤ i < length a → [a[i]/it]exp a→forAll(it1, it2: DT | exp) ∀ i j: int. 0 ≤ i < length a ∧ 0 ≤ j < length a → [a[i]/it1,a[j]/it2]exp a→exists(it: DT | exp) ∃ i: int. 0 ≤ i < length a ∧ [a[i]/it]exp a→exists(it1, it2: DT | exp) ∃ i j: int. 0 ≤ i < length a ∧ 0 ≤ j < length a ∧ [a[i]/it1,a[j]/it2]exp a→one(it: DT | exp) ∃ i: int. 0 ≤ i < length a ∧ [a[i]/it]exp ∧ (∀ j: int. 0 ≤ j < length a ∧ j <> i → [a[i]/it]exp <> [a[j]/it]exp) a→isUnique(it: DT | exp) ∀ i,j : int. 0 ≤ i < length a ∧ 0 ≤ j < length a ∧ i <> j → [a[i]/it]exp <> [a[j]
/it]exp Table 1. ocl logical property verification operations mapping to Why expressions

Value extraction iteration operations

Iteration operations also allow extracting values from a collection: according to the satisfaction (select) or not (reject) of a property; or by applying a treatment on every element of a list (collect). Value extraction operations are more complex to model as they do not only provide a single boolean value as output, they actually compute a list of elements.

Iteration operations semantics Iteration operations apply on collections and compute filtering of the collection values and/or mapping of functions on the collection values. We decide thus to represent a collection as the c, p, f tuple. Its semantics is provided in [START_REF] Anastasakis | On challenges of model transformation from UML to alloy[END_REF].

c, p, f = {f (v)|v ∈ c, p(v)} (1)
According to the previous notation, we define the initial value of a collection as in [START_REF] Achim | Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5. Archive of Formal Proofs[END_REF] where ⊤ is the predicate returning true and id the identity relation.

c = {v 1 , ..., v n } = c, ⊤, id (2)
The definition of iteration operations is hence specified as in [START_REF] Achim | HOL-OCL: A formal proof environment for UML/OCL[END_REF]. From these definitions, we extract the implementations for iteration operations using the Why language. We provide in the following two possible implementations.

c, p, f → select(e|ϕ) = c, p ∧ [f /e]ϕ, f c, p, f → reject(e|ϕ) = c, p ∧ ¬[f /e]ϕ, f c, p, f → any(e|ϕ) = c, p, f → select(e|ϕ) → f irst() c, p, f → collect(g) = c, p, f • g (3)
Iteration operations as first order logic constructs Providing an implementation for iteration operations can be done using first order logic constructs.

It is then required to generate a different function for each iteration operation call and then to write a call to the generated function in the translated ocl operation code. Using first order logic to provide an implementation for iteration operations is quite straightforward. Nevertheless, the implementation and verification of the generation process might be quite complex. Indeed the generated code complexity might increase when complex expressions are used in the body of the iteration operation.

Iteration operations as higher order logic construct An alternative approach for the implementation of iteration operations is to rely on higher order logic to represent the operations in Why. An example of such formalisation is provided in Listing 1.1 for the select iteration operation. The select function in Why takes two arguments, the first one is the collection on which the operation is applied and the second one is the predicate that must be used in order to select the elements of the collection. In addition to the function definition, we provide a set of lemmas verified with the Why3 platform generating proof obligations discharged using smt solvers and proof assistants. In the case of the select function, part of the lemmas are verified using smt solvers and others have been verified using the Coq proof assistant. We provide in Figure 2 a report generated with the Why3 toolset for these verifications. The verification effort required for the verification of the iteration operations (writing of the specification and achieving the proof) is rather similar to the one needed for the verification of collection operations. Details regarding the formalisation and the proofs for the other ocl collection operations is provided in the first author PhD thesis work5 , and our website 6 .

In order to use the iteration expressions, one must provide a body containing the condition or the operation to apply on each element of the collection. The condition body of the reject, select and anyAs operations is translated as an inlined predicate whereas the function body of the collect operation is translated as an in-lined function. In-lined predicates and functions are provided as the second argument of their respective WhyML function call. Contrary to the first order operations, there is no need here to keep track of the variables used in the iteration operation as the in-lined nature of the function call makes their definition directly available.

Additional restrictions on the support of the OCL language

In the previous sections, we gave the translation rules for a subset of the ocl language. ocl provides a well known syntax for software engineers. In addition, this subset of the language eases and secures the constraints writing process relying on first order logic by including only well known and standard functions and operations on classical data types. A major restriction in our implementation of the ocl language is the absence of the specific invalid and null values. This is related to the binding to the data part of the dsml and to the formal verification introduced by the Why3 toolset. The invalid value is used for the modeling the failure of an operation, we advocate that if such an operation is equipped with pre-conditions then the invalid value can never be an output of the operation and is thus not necessary. This value is also used when ocl is bound to uml or mof to model optional attributes or references that are not defined in the model instances. We advocate that an empty collection is also a good model for this case. Regarding the null value, it is used in order to model an object that does not exists. Once again this should not happen in a formalisation of the language but it could be handled by relying on an option type. Adding the support for these specific values will have a strong impact on the Why implementation of the ocl constructs. Indeed, these specific values will need to be taken into account in the implementation of all functions and on the related proofs. There are technical difficulties in implementing these values as shown by [START_REF] Achim | Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5. Archive of Formal Proofs[END_REF] but it is possible to overcome most of them.

The limitations we applied on the formalisation of ocl have the advantage of providing a simpler, well defined subset of the language enforcing the dsml developer to rely mostly on common knowledge ocl constructs and thus avoid the problems related to the use of more complex constructs such as the closure operator. These operators may cause some misunderstandings; make the specification more obscure; and make its verification more complex.

The subset of ocl we currently handle could be extended if required by the integration to other dsmls as shown by [START_REF] Achim | Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5. Archive of Formal Proofs[END_REF]. We will try to keep it as limited as possible.

Related Works

Many works in the literature target the formal verification of dsmls. We will only focus on those where the ocl language is used either in the dsml specification and/or as a language component part of the dsml; and is included in the verification process. Most of the formal dsml verification processes including ocl are related to its use in the context of uml specifications.

Our approach is close to the one proposed in the hol/ocl project [START_REF] Achim | HOL-OCL: A formal proof environment for UML/OCL[END_REF][START_REF] Achim | Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5. Archive of Formal Proofs[END_REF]. Its authors target the formal verification of uml specifications including ocl constraints and contracts by providing a bridge to the hol/ocl whose formal foundations relies on the Isabelle proof environment. This work is specifically remarkable by its coverage of ocl and has highly contributed to the ocl community by providing formal specifications for the language that raised numerous legitimate questions regarding the semantics of ocl operations and constructs leading to the clarification of the standard. Our work takes a different angle and aims at the verification of dsmls in general whereas the hol/ocl one is focused on uml. We also differ by our use of the Why3 toolset instead of Isabelle. Both toolsets allows for the use of smt solvers for the automatic verification of properties but Why3 can be used as a bridge to many more different solvers and proof assistants including Isabelle. Why3 also benefits from its simpler high level syntax. It is our belief that by relying on the Why3 toolset, a wider range of users will be able to actually perform formal verifications of properties as the Why and WhyML languages are simpler to apprehend than Isabelle. Our work targets a significantly smaller coverage of the ocl standard that allows avoiding key semantics issues like the invalid and null values. This has not been a limiting issue for our use up to now. However, we are far from the completeness of the hol/ocl project and we do not plan to reach it.

Clavel et al [START_REF] Clavel | Checking unsatisfiability for OCL constraints[END_REF][START_REF] Dania | OCL2FOL+: coping with undefinedness[END_REF] provides a translation from ocl to first order logic (fol). Automated theorem provers and smt solvers are then used to check the unsatisfiability of the generated fol constructs. This work supports the null and invalid values. It focuses on the verification of ocl constraints expressed on data models. Our work is more focused on the verification of ocl as a language component for dsmls. The same difference can be found in the work by Lano et al [START_REF] Lano | Uml to b: Formal verification of object-oriented models[END_REF] where uml class diagrams and a subset notational variant of ocl (LOCA) are handled and verified through a transformation to the B language.

uml/ocl specifications are translated to sat solving format by Soeken et al [START_REF] Soeken | Verifying UML/OCL models using boolean satisfiability[END_REF][START_REF] Soeken | Encoding OCL data types for sat-based verification of UML/OCL models[END_REF] or integrated in the USE toolset by Kuhlmann et al [START_REF] Kuhlmann | Extensive validation of OCL models by integrating SAT solving into USE[END_REF]. Another formalism for the automated verification of specifications is the PVS theorem prover. Kyas et al in [START_REF] Kyas | Formalizing UML models and OCL constraints in PVS[END_REF] provides a lightweight translation of ocl and uml state machines and class diagrams. Each of these approaches uses different formalism for the formal verification with efficient verification results but are tied up to the use of this specific formal verification technique. Our work benefits from the wider range of formal verification toolsets that the Why3 platform provides including most of the ones used in these works. Some other approaches have been used in order to formally model uml/ocl specifications as in the works from Kyriakos et al [START_REF] Anastasakis | On challenges of model transformation from UML to alloy[END_REF] and Cunha et Al [START_REF] Cunha | Translating between alloy specifications and UML class diagrams annotated with OCL[END_REF] on the UML2Alloy tool. These provide means for the verification of uml/ocl specifications and put a specific emphasis on the feedback of the verification result to the dsml user. We did not focus on the feedback from solvers in our work but it would be possible as the Why3 toolset provides access to smt solvers with counter-example generation capabilities.

Conclusion and Future Works

We have described a lightweight formalisation of the ocl language in Why3 where the limitations have been identified and discussed. We have briefly detailed an example of dsml where ocl is used as a component language. We rely on our formalisation of ocl to conduct the automated verification of high level properties on the dsml instances.

It is our belief that the dsml community would benefit from such a formalisation as it allows to improve the quality of model verifications by relying on formal verification techniques; it is based on the use of the Why3 toolset that eases the writing of properties and is more accessible for industrial practitioners than other formal verification platforms (like proof assistants for example) yet still supporting their use. This accessibility is very likely to help on the adoption of formal methods as a natural and standard verification technique.

The work conducted here was mostly driven by the verification of a specific dsml: the BlockLibrary specification language. The next step is to ease the integration of ocl as a component language for other dsmls. Specifically, we will focus on the adaptation of the translation of the dsml structure to Why3 which is currently done manually. We plan on providing a translation from meta-models instances of mof or Ecore to generically transform any dsml specification into a set of Why theories. The translated theories will then be used in conjunction with our formalisation of ocl to conduct verification activities on the dsml instances.

We are investigating a larger subset of ocl that still allows for an efficient automatic verification of dsml properties. We will specifically focus on the handling of any type of collections; the constructs that still need handling (tuples); and collection operations we did not implement yet. Handling the special invalid and null values could be done by relying on an approach close to the one provided by Dania et al in [START_REF] Dania | OCL2FOL+: coping with undefinedness[END_REF].

In our BlockLibrary dsml the blocks semantics is specified using an action language. Such a semantics is then translated as a WhyML function. We could have used an already existing action language like fUML/alf [START_REF] Perseil | ALF formal[END_REF] for example. By relying on a custom language, we simplified the translation work by limiting it only to the constructs that were needed. We plan, as proposed for a subset of ocl, on providing a formalisation for a subset of such an action language component. This will then be used for the verification of the semantics definition for dsmls and will thus complete the dsml verification approach.

Fig. 1 .

 1 Fig. 1. Delay block specification using the BlockLibrary dsml

  function select ( l : list oclType ) ( p : HO . pred oclType ) : list oclType = match l with | Nil -> Nil | Cons hd tl -> if p hd then Cons hd ( select tl p ) else select tl p end lemma select_nil : forall p : HO . pred oclType . select Nil p = Nil lemma s e l e c t _ c o n s _ n i l _ v e r i f i e d : forall e : oclType , p : HO . pred oclType . p e -> select ( Cons e Nil ) p = Cons e Nil lemma s e l e c t _ c o n s _ n i l _ n o t _ v e r i f i e d : forall e : oclType , p : HO . pred oclType . not ( p e ) -> select ( Cons e Nil ) p = Nil lemma s e l e c t _ c o n s _ v e r i f i e d : forall e : oclType , l : list oclType , p : HO . pred oclType . p e -> select ( Cons e l ) p = Cons e ( select l p ) lemma s e l e c t _ c o n s _ n o t _ v e r i f i e d : forall e : oclType , l : list oclType , p : HO . pred oclType . not ( p e ) -> select ( Cons e l ) p = select l p lemma s el e c t _ m e m_ r e d u c : forall l : list oclType , b : oclType , p : HO . pred oclType . mem b ( select l p ) -> mem b l lemma select_mem : forall l : list oclType , b : oclType , p : HO . pred oclType . ( mem b l /\ p b ) -> mem b ( select l p ) lemma se lect_not _mem : forall l : list oclType , b : oclType , p : HO . pred oclType . ( mem b l /\ not ( p b )) -> not ( mem b ( select l p ))

  Listing 1.1. Select iteration operation formalisation in Why using higher order logic Select verification through smt solvers and proof assistants (time in seconds)

	Proof obligations	Alt-Ergo-Pro (1.0.0) Coq (8.4pl3)
	lemma select nil	0.03
	lemma select cons nil verified	0.04
	lemma select cons nil not verified	0.05
	lemma select cons verified	0.03
	lemma select cons not verified	0.04
	lemma select mem reduc	2.40
	lemma select mem	2.31
	lemma select not mem	2.01
	Fig. 2.

http://www.omg.org/spec/ALF/Current

http://www.dieumegard.net/thesis/Thesis-Arnaud Dieumegard.pdf

http://block-library.enseeiht.fr

http://block-library.enseeiht.fr/html

http://www.dieumegard.net/thesis/Thesis-Arnaud Dieumegard.pdf

http://block-library.enseeiht.fr


Brahim Hamid
email: hamid@irit.fr

Interplay of Security&Dependability and Resource using Model-driven and Pattern-based Development

Keywords: Security, Dependability, Resource, Pattern, Model-driven Engineering, Embedded Systems Engineering

Several frameworks have been proposed

to help designers of embedded system applications. However, we currently lack methodological tool support to take into account the interplay between secu-rity&dependability and resource properties. In this work, we propose a modeling environment which associates model-driven paradigms with security and dependability patterns to ensure that the combination of security and dependability solutions fit on the targeted hardware platform. The resulted framework will serve as a tool to estimate the resources consumed by the security and dependability solutions at early stages of design to help the designer to avoid resource conflicts at run-time. In addition, we provide an architecture for development tools to support the design and the analysis of pattern-based secure and dependable applications. Finally, we apply it in practice to a use case from railway domain with strong security and dependability requirements.

I. Introduction

Embedded systems share a large number of common characteristics, including real-time and physical constraints (e.g. temperature), as well as energy efficiency requirements [START_REF] Henzinger | The embedded systems design challenge[END_REF]. Furthermore, many embedded systems also have assurance requirements, ranging from very strong levels involving certification (e.g. DO178 and IEC-61508 for safety-relevant embedded systems development) to lighter levels based on industry practices. Consequently, the conception and design of embedded systems is an inherently complex endeavor. In particular, non-functional requirements from Security and Dependability (S&D) are exacerbating this complexity. This is especially true for Resource Constrained Embedded Systems (RCES), as they refer to systems which have memory and/or computational processing power constraints. The generation of RCES therefore involves specific software building processes.

Security&Dependability solutions may have a vast impact to the rest of the system, for example an improved rigorous authentication mechanism may degrade perfor-mance; and vice-versa system resource restriction may potentially compromise security, for example using light cryptographic mechanisms is usually performed to boost performance but may pose security risks. Therefore the system's resource constraints and S&D cannot be considered in isolation, but they need to be studied in tandem as quality attributes. However, in many cases security and dependability engineering and system engineering are "islands", in the sense that the disciplines work independently of one another. In addition, in system engineering, S&D may be compromised in several system layers and lifecycle stages. Usually, S&D are considered when design decisions are made leading to potentially conflicting. This brings tremendous challenges during system integration and evolution. The interplay between requirements engineering and architecting has been well established [START_REF] Nuseibeh | Weaving together requirements and architectures[END_REF] but we lack methods and tools to support it [START_REF] Galster | Views on software engineering from the twin peaks of requirements and architecture[END_REF].

Model-based system engineering and Model-Driven Engineering (MDE) promote the integration of S&D issues into the complete engineering process [START_REF] Hamid | Model-Driven Engineering for Trusted Embedded Systems Based on Security and Dependability Patterns[END_REF]. When S&D requirements are determined, architecture and design activities are conducted using modeling-techniques and tools for higher quality and seamless development. On the other hand, the integration of S&D features using this approach requires the availability of system architecture expertise, application domain specific knowledge and S&D expertise at the same time to manage the potential consequences of design decisions on the S&D of a system and on the rest of the architecture attributes. For instance, at architectural level, security means to have a mechanism (it may be a component or integrated into a component). Hence capturing and providing this expertise by means of S&D patterns can enhance systems development by integrating them in the different development life-cycle stages.

In [START_REF] Hamid | Enforcing S&D Pattern Design in RCES with Modeling and Formal Approaches[END_REF], we have studied pattern modeling frameworks and proposed semi-formal representation of security and dependability patterns using metamodeling techniques and provided accompanying formal specification to validate their security and dependability properties. In this paper, we go one step further: we propose a modeling framework for the specification and analysis of secure and dependable pattern-based software and system architecture for RCES using patterns. Special emphasis will be devoted to promote the particularly challenging task of efficiently integrating security and dependability solutions, within the restricted available resources for embedded system, by design to foster reuse. At the core of the framework is a set of Domain-Specific Modeling Languages (DSML) [START_REF] Gray | Domain-Specific Modeling[END_REF] and model transformations that allow modeling a set of modeling artifacts, including pattern, resource and property models. The pattern is the first class citizen of these modeling artifacts to describe security and dependability solution. The resource will capture the computing system platform and the property will allow to govern the use of patterns and their analysis for reuse.

The rest of the paper is organized as follows. In Section II, we present a review of the most important related work. In Section III, we outline our overall approach for pattern-based engineering methodology. Section IV presents the management of S&D patternbased architecture during the software development lifecycle with analysis activities. In Section V, we describe an model-based development framework to support the methodology. Section VI describes the usage of the defined modeling framework in the context of patternbased RCES applications through a case study from railway domain. Finally, section VII concludes and draws future work directions.

II. Related Work

The ideas of system architecture, security and dependability modeling and analysis are not new but, to the best of our knowledge, the interplay and integration of system security&dependability and the rest of the architecture is. In this section we describe prior work in these areas and discuss their relationship to our work.

There has been a renewed interest in how to support the Twin Peaks model [START_REF] Avgeriou | Relating Software Requirements and Architectures[END_REF], in a wide range of aspects such as: theoretical frameworks for relating requirements and architecture, tools and techniques such as goaloriented inference and uncertainty management, problem frames and service composition. There has also been a discussion on the similarities between the problem and solution space and the way of interpreting requirements and design decision based on the viewpoint of a stakeholder [START_REF] De Boer | On the similarity between requirements and architecture[END_REF]. More relevant to the topic of this paper, there are also approaches for applying the Twin Peaks model in the context of security [START_REF] Heyman | The security twin peaks[END_REF]. [START_REF] Herzig | An approach to identifying inconsistencies in model-based systems engineering[END_REF] presents an approach for the identification of inconsistencies of models in the context of Model-based System Engineering using pattern matching and multi-graphs based formalism.

Several proposals exist in the literature to deal with patterns for security and dependability concern. They allow to solve very general problems that appear frequently as sub-tasks in the design of systems with security and dependability requirements. These elementary tasks include secure communication, fault tolerance, etc. A framework for the development of dependable software systems based on a pattern approach is proposed in [START_REF] Tichy | Design of selfmanaging dependable systems with UML and fault tolerance patterns[END_REF]. The pattern specification consists of a service-based architectural design and deployment restrictions in form of UML deployment diagrams for the different architectural services. [START_REF] Giacomo | Using Security and Dependability Patterns for Reaction Processes[END_REF] reports an empirical experience, about the adoption and eliciting S&D patterns in the Air Traffic Management (ATM) domain, and show the power of using patterns as a guidance to structure the analysis of operational aspects when they are used at the design stage. [START_REF] Fernandez | Software Engineering for Secure Systems: Industrial and Research Perspectives[END_REF] presented an overview and new directions on how security patterns are used in the whole aspects of software systems from domain analysis to the infrastructures.

In this paper, our aim is to support the interplay between S&D solutions and the resource constraints of the system using property model as an intermediate model. We will provide a set of domain-specific modeling languages and metamodels that will support software engineers in specifying the system constraints and requirements for the security and dependability and resource constraints interactions. As part of this objective we will focus on patterns to describe security and dependability solutions and on resource models to specify customized system and software architectures considering different concerns (e.g. target platforms, S&D quality attributes required by applications, etc.).

III. Approach: Contribution to the modeling of S&D applications

Security and dependability are not building blocks added to an application at the end of the life cycle. It is necessary to take into account these concerns from the requirement to the integration phases. From another perspective, in system engineering, security and dependability may be compromised in several system layers. Usually, security and dependability are considered when design decisions are made leading to potentially conflicting design requirements. The integration of security and dependability features requires the availability of a system architect, an application domain specific knowledge and a security and dependability expert at the same time to manage the potential consequences of design decisions on the security and on the dependability of a system and on the rest of the architecture. For instance, at architectural level, security means to have a mechanism (it may be a component or integrated into a component).

We promote a new discipline for system engineering using a pattern as its first class citizen, towards meeting our wider objective: Pattern-Based System Engineering (PBSE). Therefore, PBSE focuses on patterns and from this viewpoint addresses two kinds of processes: the process of pattern development and the process of system development with patterns. The main concern of the first process is designing patterns for reuse and the second one is finding the adequate patterns and evaluating them with regard to the system-under-development's requirements. As well, we add a repository as a tier which acts as intermediate agent between these two processes. A repository should provide a modeling container to support modeling artifacts life-cycle associated with different methodologies.

The conceptual vision of our process model is visualized in Fig. 1. In this vision, the developer starts with the system specification fulfilling the requirements. In a traditional approach (non pattern-based approach) the developer would continue with the architecture design, module design, implementation and test. In our vision, instead of following these phases and defining new modeling artifacts, that usually are time and efforts consuming as well as errors prone, the system developer merely needs to select appropriate patterns from the repository and integrate them into the model of the system under development. Once the repository1 is available, the usage of this process proceeds as follow (the numbers in parentheses correspond to the numbers in Fig. 1). The developer creates a model representing the target platform importing appropriate resource models from the repository (1). For the software part, the system developer executes the search/select actions from the repository to import patterns building a pattern system configuration (2). For each of these configurations, a mapping through

IV. S&D Pattern-based Architecture Modeling and Analysis

In our context, we have identified three kind of modeling artifacts: (1) resource models to describe platforms, (2) S&D patterns to describe software and system security and dependability solutions and (3) property models as intermediate models to serve primarily to govern the use of patterns and to evaluate their level of security as well as their resource consumption for analysis and reuse, with regard to the targeted platform. This approach aims to define an engineering discipline for S&D applications that is adapted to resource-constrained embedded systems. We now present a set of definitions and concepts that might prove useful in understanding our approach.

Adapting the definitions of [START_REF] Schumacher | Security Engineering with Patterns -Origins[END_REF], we propose the following:

Definition 1 (System of S&D Patterns.): We define a security and dependability system of patterns as a collection of security and dependability patterns forming a vocabulary. Such a collection may be skillfully woven together into a cohesive whole that reveals the inherent structures and relationships of its constituent parts toward fulfilling a shared security and dependability objective.

Definition 2 (System of S&D Patterns Configuration): A system of S&D patterns configuration is a subset of a system of patterns composed of a list of S&D patterns and a list of relationships between these S&D patterns. It will be used to specify one possible structure of an application based on S&D patterns which will be deployed on a platform.

In the following, we show how we integrate a pattern from the input pattern system (i.e. from the repository) in pattern system configuration using the potential relationships between patterns. Then, we describe the analysis in terms of resource consumption to help during the pattern selection activity regarding the target platform. Mainly, we focus on the support of consistency between S&D architectural design decisions and platform resource models through patterns.

A system of pattern is composed of a set of patterns and their relationships (see Definition 1). Let S be a system of patterns. We denote by P (S) and R(S) the set of patterns and the set of the relationships of the system of patterns S, respectively. Each relationship is associated with a relationship type [START_REF] Noble | Classifying relationships between objectoriented design patterns[END_REF], denoted by ref erenceKind, and each pattern is associated with a list of its relationships, denoted by ref erences. Let Sc and Si denote the complete system of patterns and the initial configuration of the system of patterns, respectively. To define a set of system of patterns configurations, denoted by Sg, we propose in Listing 1 a simple algorithm called conf igurationGen. This algorithm takes as input Sc and Si and a ref-erenceKind from R(Sc) to find further configurations which are equal to Si with respect to the relationship (i.e. referenceKind). The base of the system of patterns (Si) is parsed and for each pattern in this system equal patterns (with respect to the referenceKind) are looked up in the complete system of patterns (lines 3 and 4). If a pattern is found, a new configuration (newConf ig) is generated from the base system (line 7) and the pattern (P attern) from Si is replaced by the equal pattern (ref erencedP attern) from Sc. If multiple patterns are equal to a pattern in the base system, multiple configurations (one for each equal pattern) are generated. This algorithm allows to generate equal (e.g. similar, alternative) pattern system configurations and, later on, to analyze these different configurations.

1 A l g o r i t h m c o n f i g u r a t i o n G e n

B. Pattern-based System Model Analysis

Once the platform was specified using resource models, the analysis activity will be used to calculate resource consumption values and to incorporate these information into system models. For that, we provide in Listing 2 a simple algorithm to calculate the resource usage of a pattern system configuration (Sg) for a platform (R). This algorithm parses the used patterns for their consumption of different resources defined in the platform model (e.g. memory, processing power) and adds these up. The result is then injected into the platform model. For each identified property, the algorithm loops over all the patterns composing the system of patterns configuration (Sg). For each pattern (line 5), all its properties' categories (line 6) are compared to the category of the R resource property, and if matching (line 7) the values are summed up (line 8). The result is then stored as the value of the value of the platform resource property.

V. Model-Based Development (MBD)

In this section we describe an MDE framework to support the previous approach. We use metamodeling and model transformation techniques for the specification and analysis of secure and dependable system and software architecture. However, the approach does not prescribe a fixed set of metamodels and model transformations to be used. As mentioned earlier, the approach only focuses on security and dependability requirements that directly influence the available platform resources.

A. Artifacts Modeling Languages

Here, we provide a description of a set of modeling languages for the specification of the identified set of modeling artifacts: S&D patterns, property and resource models. As we shall see, S&D and resource models are used as model libraries to define the S&D and resource properties of the pattern. Therefore, a pattern can be stored in a repository and can be loaded according to the desired S&D and resource properties.

1) A Metamodel for Non-Functional Properties (GPRM).: The Generic PRoperty Metamodel (GPRM) is a metamodel defining a new formalism for describing property libraries including units, types and property categories. The following paragraph details the meanings of the principal classes of the GPRM Metamodel, which is depicted with Ecore notations in Fig. 2.

• GprmProperty. A property is a basic attribute shared by all members of an artifact (pattern, resource, etc).

As we shall see, it will be used to define pattern and resource properties (see SERM and SEPM metamodels). The property is defined by its category, its type and its value.

Example. CPU execution time for encryption and energy consumption for encryption are two properties (resource-related) of the pattern SecureCommSSL.

• GprmPropertyCategory. A property category is a classification for properties. Its role is to group all the properties sharing common characteristics. These characteristics may depend on the user or application domain viewpoint. A category supports a set of types that define the nature of the property, it can also be defined based on other categories by specialization. A category is defined with at least one default type.

Example: CPUTime is a category of resource properties and Authenticity is a category of S&D properties.

• GprmResourceCategory. A resource category is a classification for resources. Its role is to group all the resources sharing common characteristics. These characteristics may depend on the user or application domain viewpoint. The main categories are those related to computing, data storage and to energy consumption. However other categories may be defined such as peripheral, sensor, actuator, etc. A category may also be built based on existing categories by specialization.

2) A Metamodel for Resource (SERM).:

In the development context defined in our approach, embedded platforms are seen as a composition of (hardware) resources. Resources are pieces of the platform and can be combined and linked together without having an external observable state. The System and Software Engineering Resource Metamodel (SERM) is a metamodel for describing resources and their properties, as described with Ecore notations in Fig. 3. The meanings of the principal classes are more detailed in the following paragraph.

• SermResource. Is a modeling artifact which represents a piece of the platform. It defines a set of parameters that will be later used by the framework to automate the analysis of applications based on S&D patterns.

Example. IntelAtom Z530 and DDR2 RAM are two hardware resources for computing and data storage, respectively.

• SermResourceCategory. It is an GprmResourceCategory denoting a classification of a resource. Example. As computing resource categories we can define CPU, FPGA, DSP, etc. Therefore, the IntelAtom Z530 belongs on • SermProperty. It is an GprmProperty denoting a particular characteristic of a resource.

3) A Metamodel for S&D Patterns (SEPM).:

The System and Software Engineering Pattern Metamodel (SEPM) is a metamodel for describing S&D patterns, and constitutes the base of our pattern modeling language. Here we consider patterns as sub-systems that expose services (via interfaces) and manage S&D and Resource properties (via features) yielding a unified way to capture meta-information related to a pattern and its context of use. The following paragraph details the principal concepts of the SEPM metamodel to specify an S&D pattern, as described with Ecore notations in Fig. 4.

• SepmPattern. This block represents a security pattern as a subsystem describing a solution for a security particular recurring design problem that arises in specific design context. A SepmPattern defines its behavior in terms of provided and required interfaces.

• Interface. A SepmPattern interacts with its environment with Interfaces. We consider two kinds of interface: -SepmExternalInterface. Allows implementing interaction with regard to the integration of a pattern into an application model or to compose patterns. -SepmTechnicalInterface. Allows implementing interaction with security primitives and protocols, such as encryption, and specialization for specific underlying software and/or hardware platforms, mainly during the deployment activity.

• SepmProperty. Is an GprmProperty denoting a particular characteristic of a pattern related to the concern it is dealing with and dedicated to capture its intent in a certain way. For instance, security and dependability properties.

Example. We illustrate the usage of the SEPM for specifying a pattern with the example of secure communication pattern based on SSL 2 mechanism. Here, we specify an S&D property: "authenticity of sender and receiver". To type the category of this property we use a category from the earlier defined in the S&D category library: Authenticity. Moreover, we identify some resource properties, such as "CPU resource time for encryption" and "CPU resource time for authentication" that belong to category CPUTime, and "extra energy cost for encryption" and "extra energy cost for authentication" that belong to category PowerConsumption. 4) A Metamodel of system of patterns.: According to Definition 1, an S&D pattern system is a modeling artifact system where its constituent parts are S&D patterns and their potential relationships. In the following we detail the meanings of the principal classes of the pattern system metamodel, which is depicted with Ecore notations in Fig. 5.

• SepmSystemOfPatterns. A system of S&D patterns describes the relationships and the linkage among individual patterns (SeReference). Thus dependencies between specific problems can be considered in a comprehensive way.

• SeReferenceKind. We use an enumeration to define a set of types of links between S&D patterns as an extension of the relationships classification proposed in [START_REF] Noble | Classifying relationships between objectoriented design patterns[END_REF].

B. System of Patterns Configuration Analysis

For the analysis, we propose to use model transformations techniques to calculate resource consumption values and to incorporate the results into system models. According to the describable artifact, we introduce a new kind of properties to be described as a computable characteristic using the attribute computable (see Figure 2). Hence, the value of the property could be defined either by the designer during the design activity or by calculation during the analysis activity. In this case, the corresponding instance of GprmProperty (GPRM) has the computable attribute set to "true". The overview of the framework's transformations is shown in Fig. 6. The concepts of the transformations are expressed (i.e. Transformation Specification) using the Source Metamodel(s) and the Target Metamodel(s). Once specified, transformation is run (i.e. Transformation execution) taking as input the Source Model(s) and producing as output the Target model(s).

!! "" # $ % & ' ( ' ) ) ) # ) & * " " " "

C. Design and Analysis Tools

Using the proposed metamodels and the Eclipse Modeling Framework (EMF) [START_REF] Steinberg | EMF: Eclipse Modeling Framework 2.0[END_REF], ongoing experimental work is done with Semcomdt 3 (SEMCO Model Development Tools, IRIT's editor and platform plugins) as a Model-Driven Engineering tool-chain supporting the proposed metamodels. All used metamodels are specified using EMF. For the description of the model transformations, the QVT Operational language 4 is used. We build a set of software tools, for instance for design, for populating the repository and for retrieval and transform from the repository. Moreover, we provide tools to support the management of systems of patterns, the generation of configurations and the transformations for analysis.

The resource designer called Matho includes features supporting the design of resource category libraries, the design of platform resources, deposit to and retrieval from the repository through access tools. Although the tool allows to mix resource categories and resources in the same model (conforming to the definition of SERM metamodel), we recommend to separate these artifacts in two different models. The first is used to define the libraries of resource categories; and the second is used to describe the platform resources by importing and using the previous resource category libraries to type the resources. The pattern designer called Arabion is used to populate the repository with patterns conforming to SEPM metamodel, to model the system of patterns and to derive configurations from systems of patterns.

Using the algorithm proposed in IV-A, we generate a set of configurations that will be simulated with the platform in order to select the ones that give the best resources consumption trade-off. To traverse the model of the platform, the pattern system configuration and to perform calculations of resource consumption, such as depicted in Listing 2, we developed a M2M transformation using the Eclipse implementation of QVTO.

VI. A Case Study

We demonstrate the applicability of our proposed framework through the Safe4Rail demonstrator [START_REF] Teresa | Specification of Platform[END_REF] which is a simplified version of a real ETCS (European Train Control System) signaling, control and train protection system. The main functionality of this demonstrator is to supervise that traveled speed and distance do not exceed authorized maximum values provided by the railway infrastructure. In the following sub-sections, we focus on the European Vital Computer (EVC) subsystem' platform that executes the safety application. For the sake of simplicity, many functionalities of this case study have been omitted. As we will see, the architecture will be incomplete, since the approach only focuses on the description of the system platform that directly influence the security and dependability requirements. The hardware part of this subsystem is composed of a carried board on which is installed a conga-CA board with a microprocessor (Intel Atom Z530), a RAM (DDR2 RAM) and a set of interfaces for the connections. The conga-CA is accompanied with an additional programmable resource calculation unit (FPGA-Spartran).

A. Identification of Patterns

The architects analyze system safety and security requirements and mentally identify possible architectures and safety solutions to be used. Fig. 7 shows how these patterns are interconnected to form the whole system of patterns.

B. Modeling of Safe4Rail

First, we model the platform resources using the predefined libraries of resource categories. We have used Matho which provides a tree editor for resources modeling, as shown in Fig. 8. These resources are tagged and configured using the resource category libraries and the property category libraries, so that the platform model can be built subsequently as a set of configured resources. Second, we model the application based on the selected S&D patterns. We have used Arabion following modeling steps as explained in Section V-C. This means that we have started by modeling the whole pattern system including all the patterns and the relationships between them as shown in Fig. 7. Then, we use Arabion again to build the base configuration. In our case, we have chosen an initial configuration composed of Nversion programming, VoterSW, DataAgrement, Watchdog, SafetyCommCRC, SecureCommSSL and reciprocal monitoring patterns. Finally, using the configuration generation algorithm introduced in Section IV-A, we get a set of pattern system configurations. Next, we will see how some of these configurations will be used for the resource consumption analysis.

C. Analysis of Safe4Rail Application

To describe the conduct of analysis, we have selected three configurations:

• Scenario 1: "isSimilar" configuration is obtained by replacing sofware Voter pattern by hardware Voter pattern in the "Base" configuration. • Scenario 2: "isAlternative" configuration is obtained by replacing SecureComSSL pattern by Secure-ComHMAC pattern in the "Base" configuration. • Scenario 3: "Specializes" configuration is obtained by replacing SecureComSSL pattern by Secure-ComSSLTPM pattern.

Both the system of patterns and the platform are modeled as shown previously. To calculate the whole resource consumption, we execute the M2M transformation engine, using the configuration model of this scenario and the platform model as inputs, to produce a new platform model annotated with the calculated values of the resource consumption. Table I shows a comparative view of the resource consumption of the three pattern system configurations. Of course, since the system architecture contains only elements necessary for the description of the platform, the architecture will be incomplete. However, the resulted model of the system, including platform description, system of patterns configurations and the analysis, will allow the architect to experiment and to get familiar with different possibilities and options before proceed to the next steps. Also, the resource consumption results can be used to analyze which security and dependability requirements should be implemented and which should be candidates for modification or for elimination.

VII. Conclusion and Future Work

The intended role of pattern-use is to ease, systematize and standardize the approach to the construction of software-based systems. However, the problem consists in identifying them explicitly and then selecting them for reuse. In Resource Constrained Embedded Systems (RCES) development, this means that a careful balance and trade-off analysis among Security and Dependability (S&D) requirements, patterns and available platform resources is necessary. In doing so, we propose to use metamodeling and model transformation techniques for the specification of pattern configuration and to calculate resource consumption values and to incorporate this information into system models. This allows: (1) To define a new paradigm for design and implementation based on the interplay between the S&D and resource properties; (2) To increasing S&D level of RECS products by making S&D a built-in feature while enabling a consistent architecture of a system taken into account resource constraints. Furthermore, we walk through a prototype as a set of EMF editors and a set of model transformation engines supporting the approach using Operational QVT specification. An illustration by means of a case study from railway domain is provided.

As stated earlier, the pattern-based security and dependability methodology seems to be a very interesting combination of two flavors of software and hardware design which has not been addressed sufficiently in literature. The next step of this work consists in defining a pattern-based security engineering methodology. It aims at providing the correct-by-construction integration of a design pattern into an application while offering a certain degree of liberty to the designer using it. In order to be able to validate the integration, we must have a formal specification of the pattern [START_REF] Hamid | A modeling and formal approach for the precise specification of security patterns[END_REF], i.e., its properties, constraints and related validation artifacts [START_REF] Gürgens | On a formal framework for security properties[END_REF], as input to the pattern-based development process. The architecture description needs to be extended with other type of elements, e.g., software components, connectors and deployments units. This types of elements can be used, for instance, to describe architectural security and dependability patterns [START_REF] Zdun | A catalog of architectural primitives for modeling architectural patterns[END_REF]. Concurrently, more sophisticated techniques to derive artifacts relationships can be implemented, possibly using different domains, to reduce the complexity to design pattern systems. Furthermore, the correctness of the model transformations have to be determined. Another objective for the near future is to provide automated tool support for patternbased development, preferably based on a widely known and accepted model-based approach in industry such as UML [START_REF] Omg | Unified Modeling Language[END_REF]. For that, we plan to investigate the possibility to transform our design artifacts into UML and their corresponding validation artifacts into OCL [START_REF] Omg | OCL 2.2 Specification[END_REF], which would make these patterns compatible with collections such as the one in [START_REF] Fernandez | Security patterns in practice: Building secure architectures using software patterns[END_REF].

Figure 1 .

 1 Figure 1. Pattern-based System and software Engineering

2 I

 2 n p u t : Sc , S i , r e f e r e n c e K i n d .

3

  Output : { Sg } .

4 f 9 s a v e ( ) 10 e n d i f 11 e n d f o r 12 e n d f o r Listing 1 .

 491011121 o r e a c h P a t t e r n i n t h e P( S i ) do 5 f o r e a c h R e f e r e n c e i n P a t t e r n . r e f e r e n c e s do 6 i f R e f e r e n c e . r e f e r e n c e K i n d = r e f e r e n c e K i n d 7 d u p l i c a t e M o d e l ( Sg , S i ) 8 r e p l a c e P a t t e r n ( Sg , Sc , P a t t e r n , r e f e r e n c e d P a t t e r n ) Configuration generation algorithm

1 2 I 3 InputOutput : R a s a p l a t f o r m model 4 f o r e a c h P r o p e r t y pr in R 5 f 9 e n d f o r 10 e n d f o r 11 e n d f o r Listing 2 .

 23459102 A l g o r i t h m C a l c u l a t e R e s o u r c e U s a g e n p u t : Sg a s a s ys te m o f p a t t e r n c o n f i g u r a t i o n model o r e a c h P a t t e r n p in t h e P( Sg ) do 6 f o r e a c h P . P r o p e r t y do 7 i f (P . P r o p e r t y . c a t e g o r y=pr . c a t e g o r y ) then 8 pr . v a l u e :=sum ( pr . v a l u e , P . P r o p e r t y . v a l u e ) Resource consumption computing algorithm

Figure 2 .

 2 Figure 2. The (simplified) GPRM Metamodel

Figure 3 .

 3 Figure 3. The (simplified) SERM Metamodel

Figure 4 .

 4 Figure 4. The (simplified) SEPM Metamodel

  refines. It is used to represent the refinement relationship between two patterns. -specializes. It is used to represent the specialization relationship (detail). -uses. It is used to represent the functional dependency relationship between two patterns. -isSimilar. It allows to link two patterns that perform the same functionality. This link is often used to link software patterns to their equivalent hardware patterns. -isAnAlternative. It allows to link tow patterns that solve the same problem, but propose different solutions.

Figure 5 .

 5 Figure 5. A metamodel of a system of patterns

Figure 6 .

 6 Figure 6. Overview of the framework's transformations

Figure 7 .Figure 8 .

 78 Figure 7. Architecture of complete system of patterns

Table I

 I Analysis of the three scenarios

The repository system populated with S&D patterns and models an allocation process is executed[START_REF] Galster | Views on software engineering from the twin peaks of requirements and architecture[END_REF]. The allocation supports the links between a pattern and its required resources from the platform model. The result of the allocation, as the platform model and a configuration for a model of a system of patterns, is then used for analyzing (4) the resource consumption of the patterns with regard to the resources defined in the platform model (e.g. memory, processing power). The result of the analysis is then delivered for evaluation[START_REF] Hamid | Enforcing S&D Pattern Design in RCES with Modeling and Formal Approaches[END_REF]. The developer can then use MDE techniques, such as refinement, for implementing the system using the appropriate pattern system configuration[START_REF] Gray | Domain-Specific Modeling[END_REF].

The TLS Protocol Version 1.2. rfc5246, 2008.

http://www.semcomdt.org

http://www.omg.org/spec/QVT/