[aadl]: LUTE/REAL - referencing annex elements

[Julien Delange]

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
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