loonwerks / AMASE

This is the repository for Architectural Modeling and Analysis for Safety Engineering (AMASE).
BSD 3-Clause "New" or "Revised" License
6 stars 4 forks source link

Validation of fault_activation reports invalid component name #20

Open kfhoech opened 9 months ago

kfhoech commented 9 months ago

Validation of "fault_activation" constructs in the safety annex reports error message of form "The fault component: is not a valid component name for the fault: " where the subcomponent type is an abstract component. Fault activation of such form should be allowed (not an error). It is likely that this error message is due to merely to an over-zealous validator.

A simple, self-contained example as as follows:

package Example
public
    with Base_Types;

    abstract Inner
        features
            input1 : in data port Base_Types::Boolean;
            output1 : out data port Base_Types::Boolean;
        annex agree {**
            guarantee Inner_O1 "Inner Output Follows Input" :
                output1 = input1;
            node stuck_false (in1 : bool, trigger : bool) returns (out1 : bool);
            let
                out1 = if trigger then false else in1;
            tel;
        **};
        annex safety {**
            fault Inner_Output_Stuck_False "Inner component output1 is stuck false" : stuck_false {
                inputs: in1 <- output1;
                outputs: output1 <- out1;
                disable: false;
                probability: 1.0e-10;
                duration: permanent;
            }
        **};
    end Inner;

    system Outer
        features
            input1 : in data port Base_Types::Boolean;
            output1 : out data port Base_Types::Boolean;
        annex agree {**
            guarantee Outer_O1 "Outer Output Follows Input" :
                output1 = input1;
        **};
    end Outer;

    system implementation Outer.impl
        subcomponents
            inner : abstract Inner;
        connections
            c_in1 : port input1 -> inner.input1;
            c_out1 : port inner.output1 -> output1;
        annex agree {**
            eq inner_failed : bool;
        **};
        annex safety {**
            fault_activation: inner_failed = Inner_Output_Stuck_False@inner;
            analyze: max 2 fault 
        **};
    end Outer.impl;

end Example;