search

loonwerks / AGREE

Assume-Guarantee REasoning Environment
BSD 3-Clause "New" or "Revised" License
12 stars 5 forks source link

AGREE shall generate warning for AADL n-to-one connectivity #45

Closed cong-liu-2000 closed 2 years ago

cong-liu-2000 commented 3 years ago

The AADL supports n-to-n connectivity for event and event data ports. But n-to-one connectivity could introduce non-deterministic behavior. AGREE shall generate warning to make sure this is user's intent.

kfhoech commented 3 years ago

Fan-in is illegal in AADL and the Osate2 validator checks for it starting in v2.8.0. See Osate2 Issue #2356. As a portion of handling this issue, checks for fan-in were added to both the instance model and to the declarative model. However, the checks on the declarative model were removed due to potentially causing confusion to the user.

In handling AGREE Issue #30 we considered the question of fan-in. Since Osate2 generates an error message on the instance model the redundant check in the AGREE validator was removed. An AGREE test case observes that Osate2 continues to generate the error for fan-in connection instances.

Things get more complicated for event connections and event data connections. The AADL semantics are not clear in that if multiple events may occur simultaneously. If they can, it is further unclear how response to multiple events is ordered. Are the events queued? If so, in what order? If one preempts the others, how is the preemption priority specified?

AGREE forbids fan-in regardless of port type, but checks for it only at translation time, deferring to Osate2 for validation check.

The open question is whether we wish to re-instate a validator check to warn the user ahead of analysis/translation time. Such a check would need to be on the declarative model, be limited to components that have AGREE annexes, and an AGREE annex contains AGREE constructs that reference the port to which the fan-in connections are made. Such a check would be fairly expensive in computation in that it would need to check not only the port in question, but all containing components and all ancestors of these.

kfhoech commented 2 years ago

Since the OSATE AADL2 validator now checks for this problem and AGREE throws an error in translation if the problem is present in the model under analysis, this issue appears to be resolved without further change.