[aadl]: LUTE/REAL - referencing annex elements

Fri Nov 15 11:08:53 EST 2013

Hi Julien,

Thanks for the clarification; I do not see off hand any technical reason
why BA subcomponents can't be referenced in constraint theorems, however
I think that it is important to keep separate assertions about the
structural sanity of a model (i.e. assertions on presence/absence of
features, subcomponents and property fields, assertions on property
expressions) from assertions on behaviour (i.e. state history dependent
assertions). It would be great if you can send me a few examples of the
type of constraint theorems you would want to express using mixed AALL
core and BA references.

Cheers,

Serban

________________________________

From: Julien Delange [mailto:jdelange at sei.cmu.edu] 
Sent: November 14, 2013 12:17 PM
To: Serban Gheorghe; Pierre Dissaux; sae-aadl-users at lists.sei.cmu.edu
Subject: RE: [aadl]: LUTE/REAL - referencing annex elements

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.cm
u.edu] On Behalf Of Julien Delange
Sent: November 8, 2013 3:23 PM
To: Pierre Dissaux; 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
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