ErrorProcessor.aadl

package ErrorProcessor
public

annex EMV2{**
	error types
		DelayedInfo 	: type;
		NoInfo			: type;
		ErroneousInfo	: type;
		Short_circuit	: type;
		physical_shock	: type;
		AnyError		: type;
		SoftwareError	: type;
	end types;
			
	error behavior ProcessorX
		states
			Operational		: initial state;
			Malfunction		: state;
			Damaged			: state;
			Locked			: state;
		end behavior;
	
**};

end ErrorProcessor;

ErrorTypeBox1.aadl

package ErrorTypeLibBox1
public

annex EMV2{**
	error types
		DelayedInfo : type;
		NoInfo		: type;
		WrongInfo	: type;
	end types;
		
	
	error behavior Box1
		states
			Operational			: initial state;
			Failed_UnRecovarable: state;
				
	end behavior;
	
**};

end ErrorTypeLibBox1;

ErrorTypeBox2.aadl

package ErrorTypeLibBox2
public

annex EMV2{**
	error types
		DelayedInfo : type;
		NoInfo		: type;
		WrongInfo	: type;
	end types;
		
	
	error behavior Box2
		states
			Operational			: initial state;
			Failed_Recovarable	: state;
			Failed_UnRecovarable: state;
				
	end behavior;
	
**};

end ErrorTypeLibBox2;

example.aadl

package ExampleFTA
public
	with EMV2;
	with ErrorTypeLibBox1, ErrorTypeLibBox2;
	
system Box1
	features
		input1 : in event port;
		input2 : in event port;
		output1 : out event data port;
		output2 : out event data port;
		output3 : out event port;
	modes
		OFF: 			initial mode;
		Operational:	mode;
		OFF -[input1]-> Operational;
		Operational -[input1]-> OFF;
	
	annex EMV2{**
		use types ErrorTypeLibBox1;
		use behavior ErrorTypeLibBox1::Box1;
				
		error propagations
			output1 : out propagation {DelayedInfo,NoInfo,WrongInfo};
			output2 : out propagation {NoInfo,WrongInfo};
		flows
			ErrorSrc1: error source output1{NoInfo,WrongInfo} when Failed_UnRecovarable; 
			ErrorSrc2: error source output1{DelayedInfo} when Operational;
		end propagations;
				
		component error behavior
		events
			ResetEvent: recover event input2;
			UncoveredFault: error event;
		
		transitions
			tFailed	: Operational -[UncoveredFault]-> (Operational with 0.1, Failed_UnRecovarable with 0.9);	
		end component;
		
		properties
			emv2::occurrencedistribution => [ probabilityvalue => 2.0e-5;
                                             distribution => poisson;
                                            ] applies to Failed_UnRecovarable; 
            emv2::occurrencedistribution => [ probabilityvalue => 2.0e-9;
                                             distribution => poisson;
                                            ] applies to Operational;                        		
	**};
	
end Box1;

system implementation box1.i
end box1.i;
system implementation box2.i
end box2.i;

system Box2
	features 
		input1 : in  event data port;
		input2 : in  event data port;
		input3 : in  event port;
		output : out event data port;
		
	annex EMV2{**
		use types ErrorTypeLibBox2;
		use behavior ErrorTypeLibBox2::Box2;
				
		error propagations
			input1 : in  propagation {DelayedInfo,NoInfo,WrongInfo};
			input2 : in  propagation {NoInfo,WrongInfo}; 
			output : out propagation {DelayedInfo,NoInfo,WrongInfo};
		end propagations;
		
		component error behavior
		events
			ResetEvent: recover event input3;
		transitions
			tFailedRecovarable		: Operational	-[input1{NoInfo,DelayedInfo} or input2{NoInfo}]-> (Operational with 0.5, Failed_Recovarable with 0.5);
			tFailedUnrecovarable	: Operational -[input1{WrongInfo} or input2{WrongInfo}]-> (Operational with 0.5, Failed_UnRecovarable with 0.5);
			tOperational			: Failed_Recovarable -[ResetEvent]-> (Failed_Recovarable with 0.5, Operational with 0.5);	
			tFailedRevToOperatinal	: Failed_Recovarable -[input1{WrongInfo} or input2{WrongInfo}]-> (Failed_Recovarable with 0.5, Operational with 0.5);				
		end component;
		
		properties
			emv2::occurrencedistribution => [ probabilityvalue => 2.0e-5;
                                             distribution => poisson;
                                            ] applies to Failed_UnRecovarable;
            emv2::occurrencedistribution => [ probabilityvalue => 2.0e-7;
                                             distribution => poisson;
                                            ] applies to Failed_Recovarable;
           	emv2::occurrencedistribution => [ probabilityvalue => 2.0e-10;
                                             distribution => poisson;
                                            ] applies to Operational;
		**};
end Box2;

system Example
end Example;

annex EMV2{**
	error types
		SoftwareError: type;
	end types;
	type mappings ErrorMappings
	use types ErrorTypeLibBox1;
		{ErrorTypeLibBox1::DelayedInfo} -> (ErrorTypeLibBox2::DelayedInfo);
		{ErrorTypeLibBox1::NoInfo} -> (ErrorTypeLibBox2::NoInfo);
		{ErrorTypeLibBox1::WrongInfo} -> (ErrorTypeLibBox2::WrongInfo);	
	end mappings;
	
**};


system implementation Example.imp
	subcomponents
		Box1 : system Box1.i;
		Box2 : system Box2.i;
	connections
		c1: port Box1.output1 -> Box2.input1;
		c2: port Box1.output1 -> Box2.input2;
		c3: port Box1.output2 -> Box2.input2;
		c4: port Box1.output3 -> Box2.input3;
	annex EMV2{**
		use types exampleFTA;
		use type equivalence exampleFTA::ErrorMappings;
		use behavior ErrorTypeLibBox2::Box2;
		
		error propagations
			processor: out propagation{SoftwareError};
			memory: out propagation{SoftwareError};
			bus: out propagation{SoftwareError}; 
		flows
			f0: error source processor{SoftwareError};
		end propagations;			
		
		composite error behavior
			states
				[Box1.Operational and Box2.Operational]-> Operational;
				[Box1.Operational and Box2.Failed_Recovarable]-> Failed_Recovarable;
				[Box1.Failed_UnRecovarable and Box2.Operational]-> Failed_UnRecovarable;
				[Box1.Failed_UnRecovarable and Box2.Failed_UnRecovarable]-> Failed_UnRecovarable;
				[Box1.Failed_UnRecovarable and Box2.Failed_Recovarable]-> Failed_UnRecovarable;
		end composite;
		
	**};
				
end Example.imp;

end ExampleFTA;

Processor.aadl

package ProcessorX
public
	with EMV2;
	with ExampleFTA;


processor Real_Time
	features 
		Proc_port_input : requires bus access;
		Proc_port_output: requires bus access;
				
	annex EMV2{**
		use types ErrorProcessor;
		use behavior ErrorProcessor::ProcessorX;
		
		error propagations
			Proc_port_output: out propagation {DelayedInfo,NoInfo,ErroneousInfo}; 
			bindings: in propagation {SoftwareError};
			bindings: out propagation {AnyError};
		
		flows
			f0: error source bindings{AnyError};		
		end propagations;	
		
		component error behavior
		events
			whatch_dog	: recover event;
			reset		: recover event;
			High_Temp	: error event;
		transitions
			tLocked		: Operational	-[High_Temp]-> (Operational with 0.1, Locked with 0.9);
			--tFailedUnrecovarable	: Operational -[input1{WrongInfo} or input2{WrongInfo}]-> (Operational with 0.5, Failed_UnRecovarable with 0.5);
			--tOperational			: Failed_Recovarable -[ResetEvent]-> (Failed_Recovarable with 0.5, Operational with 0.5);	
			--tFailedRevToOperatinal	: Failed_Recovarable -[input1{WrongInfo} or input2{WrongInfo}]-> (Failed_Recovarable with 0.5, Operational with 0.5);
		end component;	
		
	**};
end Real_Time;

processor implementation Real_Time.impl
end Real_Time.impl;

system Bounded
end Bounded;

system implementation Bounded.impl
	subcomponents 
		ProcessorX: processor Real_time;
		BoxSoftware: system ExampleFTA::Example;
	properties 
		Actual_Processor_Binding => (reference(ProcessorX)) applies to BoxSoftware;
end Bounded.impl;

end ProcessorX;