saeaadl / emv2

AADL Error Model V2 annex language
0 stars 0 forks source link

Semantics of Composite Error Behavior state transitions #91

Open AaronGreenhouse opened 1 year ago

AaronGreenhouse commented 1 year ago

Section E.11 leaves much unsaid about exactly what transitions are implied by the composite error behavior composite state transitions. For example, it is very easy to derive a set of transitions that produce loops. Currently transition loops are not explicitly prohibited anywhere in the standard, but they have undesirable effects on many model analyses. Also the others keyword is not always expressible in analyses because its most basic expression would be the negation of the all composites state that are explicitly declared. Not all target analysis representations (e.g. fault trees) are well suited to express negation.

The simple example below consists of a system with two identical subsystems. Each subsystem can independently fail and move to a Failed state. The behavior of the top-level system is defined using composites state based on the four possible combinations of subsystem states (Normal, Normal), (Normal, Failed), (Failed, Normal), and (Failed, Failed).

A straightforward interpretation of the composite behavior suggests, for example, that it is possible to transition from (Normal, Normal) to (Normal, Failed), and then from (Normal, Failed) back to (Normal, Normal). This creates a loop. This makes it impossible, for example, building a fault tree for the example. Of course, it turns out that this backwards transition is not really possible, because it is not possible for a subsystem to transition back to normal once it is failed. How should this be factored into the composite behavior, if at all? This is tricky because it opens up the abstraction layers provided by components.


package CompositeStates
public
    annex EMV2 {**
        error behavior Simple
        events
            Fail: error event;
        states
            Normal: initial state;
            Failed: state;
        transitions
            x1: Normal -[Fail]-> Failed;
        end behavior;

        error behavior Complex
        states
            Normal: initial state;
            A_Failed: state;
            B_Failed: state;
            AB_Failed: state;
        end behavior;
    **};

    system X
        annex EMV2 {**
            use behavior CompositeStates::Simple;
        **};
    end X;

    system Top
    end Top;

    system implementation Top.i
        subcomponents
            A: system X;
            B: system X;
        annex EMV2 {**
            use behavior CompositeStates::Complex;

            composite error behavior
            states
                [A.Normal and B.Normal]-> Normal;
                [A.Normal and B.Failed]-> B_Failed;
                [A.Failed and B.Normal]-> A_Failed;
                [A.Failed and B.Failed]-> AB_Failed;
            end composite;
        **};
    end Top.i;
end CompositeStates;```
brlarson commented 1 year ago

Loops in error state machines are proper. A repair event, or activation of a cold spare can restore operation. If some tools have problems with loops, that's a tool issue, not a language issue.