Check Behavior Annex freeze and send actions against Input_Time and Output_Time 🤖

[lwrage]

Summary

The BA validator does not check the AS5506/3 Rev. A D.5 consistency rules between explicit BA input-freeze/output-send actions and the core Input_Time/Output_Time properties.

No active BA checker path was found that reads these properties while validating >>, !, or the dispatch frozen clause.

Reproduction

This issue comes from the source audit in ba/doc/conformance.md; no additional runtime reproduction was performed.

Expected behavior

Report BA freeze or send behavior that conflicts with the corresponding core timing property, while accepting equivalent specifications and cases where only one mechanism specifies the timing.

Relevant code

• ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaConsistencyRulesChecker.java.
• ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaRulesCheckersDriver.java.
• ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java — port freeze/send translation.

[lwrage]

Instance-model implementation boundary

The substantive consistency checks in this issue require the effective Input_Time or Output_Time of a particular port instance. Both properties can be supplied or overridden by contained property associations outside the classifier that owns the Behavior Annex. Therefore a source validator cannot determine whether a freeze or send action agrees with them.

The declarative pass can preserve and resolve the BA action and port reference. The actual comparison must run after instantiation, map that reference to the corresponding FeatureInstance, and query the property there. Tests should use two instances of one classifier with a contained timing-property override on only one port instance and assert different consistency results.