[aadl]: LUTE/REAL - referencing annex elements

[Julien Delange]

Hi Serban,

The intent was indeed to have the capability to include/reference Behavior Annex artifacts in a constraint theorem. I am not proposing anything and my intent was rather a message for trying to see if someone has some thoughts about it and/or already have made efforts to do so.

Hope that clarify my intent, sorry if some information were missing in my initial e-mail.

Julien.

From: Serban Gheorghe [mailto:serbang at edgewater.ca]
Sent: Tuesday, November 12, 2013 11:44 AM
To: Julien Delange; Pierre Dissaux; sae-aadl-users at lists.sei.cmu.edu
Subject: RE: [aadl]: LUTE/REAL - referencing annex elements

Hi Julien,

When we talk about "constraints", we are clearly dealing with two different audiences:  tool builders and model builders.

Real/Lute and their generalization in the current Constraint Annex language proposal are intended for engineers building real-world AADL models, not for tool builders. The approach described by Pierre is perfectly fine for tool builders, but would be very strange looking to engineers involved in using AADL (among other tools) to express design constraints on a particular subsystem they are building from scratch.

The fact that a constraint mechanism suitable for any object in the meta-model can also be used to constrain user defined classifiers or instance models, is convenient from a tool builder point of view, but it prevents adoption by the engineers involved in product development. We can easily see this by taking a look at the use of OCL as a constraint language for user built UML components, it doesn't happen very often although it could be used that way.

>From the formulation of your email it is not clear to me what your main requirement is:

1.      Pierre seems to have understood your email as an attempt to write the entire AADL core and annexes semantic rules using the constraint language (i.e. writing constraints that work for any meta-model object)

2.      I understand it differently, it seems that you are proposing to move the goal posts of the Constraint Annex to also cover the Behaviour Annex and possible other current and future Annexes, but still keep the focus on model builders ((i.e. writing design constraints for classifiers, their instances, their subcomponents and properties defined both in the AADL core and annexes)

Please clarify which interpretation is closer to your intent and what is the motivation (and do not say BOTH ! )

Cheers,

Serban

________________________________
From: sae-aadl-users-bounces+serban.gheorghe=edgewater.ca at lists.sei.cmu.edu<mailto:sae-aadl-users-bounces+serban.gheorghe=edgewater.ca at lists.sei.cmu.edu> [mailto:sae-aadl-users-bounces+serban.gheorghe=edgewater.ca at lists.sei.cmu.edu] On Behalf Of Julien Delange
Sent: November 8, 2013 3:23 PM
To: Pierre Dissaux; sae-aadl-users at lists.sei.cmu.edu<mailto:sae-aadl-users at lists.sei.cmu.edu>
Subject: Re: [aadl]: LUTE/REAL - referencing annex elements

Thanks for your quick reply. I think we should adopt a similar mechanism. As there are several discussion on a constraint annex and different implementation, I am guessing this would be a good opportunity to synchronize our efforts, especially if nobody has already implemented/handled that feature for a constraint language. In particular, a great benefit would be in reducing the work for supporting a new annex and avoid any annex-specific keyword in the constraint annex (so that the tool would not depend on a specific annex language/plug-in).





From: Pierre Dissaux [mailto:pierre.dissaux at ellidiss.com]
Sent: Friday, November 08, 2013 4:10 AM
To: Julien Delange; sae-aadl-users at lists.sei.cmu.edu<mailto:sae-aadl-users at lists.sei.cmu.edu>
Subject: Re: [aadl]: LUTE/REAL - referencing annex elements

> Dear all,

Hi Julien,

>
> We are currently investigating the use of LUTE (or REAL/any other constraint language) to check the consistency of the core AADL language with > its annex.  This would need to introduce the capability to reference the core AADL model and its additions (annexes). One application of such
> feature would provide the ability to check core components/properties (ex: the queue size of an event [data] port) according to its behavior
> description (the behavior state machine).
>
> As many of us are currently working on a constraint language, it would be interesting to know if someone has already investigated this idea
> and have some thoughts/ideas about the syntax, the reference between the two languages and the implementation of the verification engine.

In AADL Inspector (and our other tools), we are using our LMP technology (Logic Model Processing)  for implementing the model queries, the constraint rules and even model transformation rules with a single language (prolog). So we do not need LUTE or REAL, but in many cases the constraint rules look very similar.

The idea is to get a representation of the complete AADL model (core + annexes) under the form of a prolog facts base.
The fact predicates are deduced from the language meta-model constructs

Example:
  isFeature('PORT','messages_Pkg','sender','send','OUT','EVENT','NIL','NIL','NIL','352').
  ...
  isBAAction('messages_Pkg','sender','others','unnamed_A1','t','2','send','!','NIL',';','367').

This facts base is automatically generated by our AADL textual language parser (aadlrev) and it currently supports AADL v1, v2.0, v2.1, the Behavior Annex, the Error Annex v1 and the draft 0.95 of the Error Annex v2 all together.

This may act as a query language. If you asks for
isFeature('PORT','messages_Pkg','sender',F,'OUT','EVENT',_,_,_,_).
The prolog engine gives you all the out event ports in component messages_Pkg::sender (i.e. F = 'send' in previous example)

Then, it is possible to write prolog rules to implement verifications or transformations.
For instance, if I want to check that the BA action is consistent with the feature declaration, a possible (simplified) verification rule is:
isBAAction(P,T,_,_,_,_,F,'!',_,_,_), not(isFeature(_,P,T,F,_,_,_,_,_,_)), write('error').
(comma means logical AND)

Finally, it is just needed to merge facts and rules together and give that to the prolog interpreter.

The same approach can be applied to other languages, including XML/XMI, and we are currently working on a UML/MARTE facts base to implement a model transformation to AADL.

However, writing formally all the AADL rules is a huge work, so we would be happy to collaborate and investigate how this can be linked with the LUTE/REAL approach.


Pierre


>
> Thanks for any idea/suggestion,

-------------- next part --------------
HTML attachment scrubbed and removed