saeaadl / aadlv2.2

SAE AADL core language, version 2.2
1 stars 0 forks source link

Change in connection and flow in_modes clause legality rule #24

Open stevevestal opened 6 years ago

stevevestal commented 6 years ago

The current standard imposes the legality rule, "If a semantic connection may be active in a particular mode, then the ultimate source and ultimate destination components must be part of that mode." It also states "Connections can be defined to be active in certain modes or in mode transitions, as indicated by the in_modes_and_transition subclause." Something similar applies to flows.

Two concerns I have with this is that it may be complicated for the user to get all the mode declarations and clauses throughout a model consistent. Semantic connections (and flows) are declared by a chain of individual connection declarations that pass through multiple subcomponents and subject to multiple modes. What if one individual connection declaration in the chain is active in its local mode and another individual connection declaration in the chain is not? Source and destination appear in different parts of a model. Judging legality is non-local, it requires some knowledge of global SOMs.

Let me suggest an alternative semantics and legality rule that might improve usability of the language.

The alternative approach is to define the standard semantics to be that a connection is by default active in SOMs where both source and destination are active. The in_modes clause is then used as a filter (rather than partly as a filter and partly as a redundant consistency check). The in_clause could be used to omit a connection from a SOM in which it would otherwise by default be active. Given a SOM, and a list of connection declarations with their own in_modes clauses, I think it is fairly easy to check whether all individual declarations in that SOM. The semantics are that a semantic connection is active if its source, destination, and every connection declaration in its chain are all active in a SOM. This basic idea would be extended for in_transitions and flows.

buzden commented 6 years ago

Generally, I feel this idea to be good and reasonable: connection does not seem to be needed if some of features that it connects disappear. Also, this suggestion seems to make easier considering of implicit complex states of a container. For example, when a container has a connection between two features of its subcomponents and these subcomponents have these features only in some their local modes. Steve's suggestion seems to make semantics of appearance of this connection to be fairly simple: it appears only when these subcomponents have such a combination of their local modes that allows both of features to appear). This frees from obligation of expressing the container's modes in terms of combination of local subcomponent's modes explicitly (which is an obvious pain because of combinatorial explosion).

But existence of semantic connections is only one side of the problem. Another side are properties that need to be assigned to the whole semantic connection. These properties can be mode-sensitive too. And this would not be solved such easily as Steve suggests for mode-sensitive existence of connections. I brought up this problem in this issue.

reteprelief commented 6 years ago

The standard indicates that a connection without in modes "applies to all modes", i.e., is active as long as the end points of the connection are active (Steve's default interpretation). Denis brings up an interesting point about features. Is it useful to allow specification of which features are visible in a particular mode? Once we have interfaces we can consider mode specific interfaces. There is also the interplay with whether features require connections - currently we have a property to indicate that a connection is optional. Is it sufficient to consider connections active when the endpoints are active, or do we still need mode-specific connections? As Denis points out this would avoid having to introduce modes in the enclosing component to specify when connections are active.

jjhugues commented 3 years ago

This rule can only be checked at instantiation, where we build the SOMs. As Denis pointed out, there are additional issues.

There has been no progress on modes for v2.3. Probably better to defer for future revision