Analysis of AGREE models with unspecified AADL properties

[kfhoech]

The AGREE language supports accessing AADL property values from property associations attached to AADL model elements. In a multi-layered model, property associations may be specified at higher layers in the hierarchy where the property associations are assigned to subcomponents or inherited from containing components. However, when analysis is undertaken at lower layers of the model, the property associations specified or inherited from higher layer models are not in scope and the AGREE analysis terminates with an error that the property value could not be determined.

In this case is it possible to consider the property as an input with the following constraints:

1. The value is arbitrary but constant (that is, the assumption (true -> (val = (pre val)) holds.
2. Any type predicate restricting the domain of the property value also holds. e.g. the property has range constraint.

[kfhoech]

Resolved by Pull Request 115.