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.
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 [
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. 2
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 [
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[
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. 2.2
The BlockLibrary DSML structural specification
The BlockLibrary dsml [
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. 2.3
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. library Lib { type signed realInt TInt32 of 32 bits type realDouble TDouble 5 type array TArrayDouble of TDouble blocktype DelayBlock { variant InputScalar { in data Input : TDouble out data Output : TDouble } variant ICScalar {
parameter IC : TDouble default 0.0 } variant ICVector {
parameter IC : TArrayDouble } variant InternalDelay { parameter Delay : TInt32 {
invariant ocl { Delay . value > 0 } } variant ExternalDelay { in data Delay : TInt32 {
invariant ocl { Delay . value > 0 } } variant ListDelay_Scalar extends allof ( oneof ( InternalDelay , ExternalDelay ) ,
InputScalar , ICVector ) { invariant ocl { Delay . value > 1 } invariant ocl {
IC . value . size () = Delay . value } memory Mem { datatype auto ocl { Input . value } length auto ocl { DelayUpperBound . value } } variant Delay_Scalar extends allof ( oneof ( InternalDelay , ExternalDelay ) ,
InputScalar , ICScalar ) { invariant ocl { Delay . value = 1 } memory Mem { datatype auto ocl { Input . value } length auto ocl {1} 55 60 65 70 75 80 85 90 mode DelayMode_Simple implements Delay_Scalar
{ init init_Delay_Simple bal { postcondition ocl {
Mem . value = IC . value }
Mem . value = IC . value ; } compute compute_Delay_Simple bal { postcondition ocl {
Output . value = Mem . value }
Output . value = Mem . value ; } update update_Delay_Simple bal { postcondition ocl {
Mem . value = Input . value }
Mem . value = Input . value ; } } mode DelayMode_List implements
ListDelay_Scalar { init init_Delay_List bal { postcondition ocl {
Mem . value = IC . value }
Mem . value = IC . value ; } compute compute_Delay_List bal { postcondition ocl {
Output . value = Mem . value -> first () }
Output . value = Mem . value [0]; } update update_Delay_List bal { postcondition ocl { Mem . value =
Mem . value -> excluding ( Mem . value -> first () ) -> append ( Input . value ) } for ( var i =0; i < Mem . value -> size () -1; i = i +1) {
Mem . value [i] = Mem . value [i +1]; }
Mem . value [ Delay . value -1] = Input . value ; }} }
}
The lack of space prevents us to detail further this dsml and we refer the
reader to our papers[
BlockLibrary specification verification A transformation translates BlockLibrary 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 BlockLibrary 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. 3
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. 3.1
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. 3.2
OCL operations translation strategy ocl defines multiple operations that are to be applied either on primitive values – referred 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. 3.3
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. 3.4
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´e et Al [
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. 3.5
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) 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 hc, p, f i tuple. Its semantics is provided in (1).
Jhc, p, f iK = {f (v)|v ∈ c, p(v)} (1)
According to the previous notation, we define the initial value of a collection as in (2) where > is the predicate returning true and id the identity relation. (2) c = {v1, ..., vn} = hc, >, idi
The definition of iteration operations is hence specified as in (3). From these definitions, we extract the implementations for iteration operations using the Why language. We provide in the following two possible implementations. hc, p, f i → hc, p, f i → hc, p, f i → hc, p, f i → select(e|ϕ) = reject(e|ϕ) = any(e|ϕ) = collect(g) =
hc, p ∧ [f /e]ϕ, f i hc, p ∧ ¬[f /e]ϕ, f i hc, p, f i → select(e|ϕ) → f irst()
(3) hc, p, f ◦ gi 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 work 5, and our website6.
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. 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
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 [
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 [
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[
Clavel et al [
uml/ocl specifications are translated to sat solving format by Soeken et
al [
Some other approaches have been used in order to formally model uml/ocl
specifications as in the works from Kyriakos et al [
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 [
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 [