test1.aadl

package test1
public
-- inherit Occurrence Distribution
with  ErrorLibrary, EMV2, test_pkg, TestErrorLibrary;

system complete 
end complete;

system implementation complete.dual 
subcomponents
sensors: device test_pkg::sensor;
control1: system test_pkg::control;
control2: system test_pkg::control;
actuator: device test_pkg::actuator;


annex EMV2{**
use behavior TestErrorLibrary::simple;

composite error behavior
states
	[sensors.failed or actuator.failed]->failed;
	[control1.failed and control2.failed]->failed;
end composite;	
--	properties
--	  EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-4 ; Distribution => Fixed;]applies to sensors.Failed;
--    EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0003 ; Distribution => Fixed;] applies to control1.Failed;
--    EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0003 ; Distribution => Fixed;] applies to control2.Failed;
--    EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0003 ; Distribution => Fixed;] applies to actuator.Failed;

**};

end complete.dual;


end test1;

test3_1_CTMC.aadl

package test3_1_CTMC
public

with  ErrorLibrary, EMV2, test_pkg, TestErrorLibrary, test1;

system complete extends test1::complete 
end complete;

system implementation complete.dual  extends test1::complete.dual
subcomponents
sensors: refined to device sensor_error;
control1: refined to system control_error;
control2: refined to system control_error;
actuator: refined to device actuator_error;

annex EMV2{**
use behavior TestErrorLibrary::simple;

composite error behavior
states
	[sensors.failed or actuator.failed or (control1.failed and control2.failed)]->failed;
--	[control1.failed and control2.failed]->failed;
end composite;	
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;]applies to sensors.Failure;
  EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to control1.Failure;
   EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to control2.failure;
   EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to actuator.Failure;
**};

end complete.dual;
device sensor_error extends test_pkg::sensor

annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to failure;
	**};
end sensor_error;


device actuator_error extends test_pkg::actuator
annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to failure;
	**};
end actuator_error;

system control_error extends test_pkg::control
annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to failure;
	**};
end control_error;
end test3_1_CTMC;

test3_1_CTMC_complete_dual_Instance__PRISM.pm

ctmc

module complete_dual_instance
	complete_dual_instance_state: [ 0 .. 1] init 0;
	[] complete_dual_instance_state=0 -> 3.0E-7 : (complete_dual_instance_state'=1);
endmodule

formula complete_dual_instance_is_operational = complete_dual_instance_state=0;

formula complete_dual_instance_is_failed = complete_dual_instance_state=1;

formula complete_dual_instance_is_failed0 = sensorscomplete_dual_instance_is_failed | actuatorcomplete_dual_instance_is_failed | control1complete_dual_instance_is_failed & control2complete_dual_instance_is_failed;


module sensorscomplete_dual_instance
	sensorscomplete_dual_instance_state: [ 0 .. 1] init 0;
	[] sensorscomplete_dual_instance_state=0 -> 3.0E-7 : (sensorscomplete_dual_instance_state'=1);
endmodule

formula sensorscomplete_dual_instance_is_operational = sensorscomplete_dual_instance_state=0;

formula sensorscomplete_dual_instance_is_failed = sensorscomplete_dual_instance_state=1;


module actuatorcomplete_dual_instance
	actuatorcomplete_dual_instance_state: [ 0 .. 1] init 0;
	[] actuatorcomplete_dual_instance_state=0 -> 3.0E-7 : (actuatorcomplete_dual_instance_state'=1);
endmodule

formula actuatorcomplete_dual_instance_is_operational = actuatorcomplete_dual_instance_state=0;

formula actuatorcomplete_dual_instance_is_failed = actuatorcomplete_dual_instance_state=1;


module control1complete_dual_instance
	control1complete_dual_instance_state: [ 0 .. 1] init 0;
	[] control1complete_dual_instance_state=0 -> 3.0E-7 : (control1complete_dual_instance_state'=1);
endmodule

formula control1complete_dual_instance_is_operational = control1complete_dual_instance_state=0;

formula control1complete_dual_instance_is_failed = control1complete_dual_instance_state=1;


module control2complete_dual_instance
	control2complete_dual_instance_state: [ 0 .. 1] init 0;
	[] control2complete_dual_instance_state=0 -> 3.0E-7 : (control2complete_dual_instance_state'=1);
endmodule

formula control2complete_dual_instance_is_operational = control2complete_dual_instance_state=0;

formula control2complete_dual_instance_is_failed = control2complete_dual_instance_state=1;

test3_CTMC.aadl

package test3_CTMC
public

-- This uses extends and refined to

with  ErrorLibrary, EMV2, test_pkg, TestErrorLibrary, test1;

system complete extends test1::complete 
end complete;

system implementation complete.dual  extends test1::complete.dual
subcomponents
sensors: refined to device sensor_error;
control1: refined to system control_error;
control2: refined to system control_error;
actuator: refined to device actuator_error;

annex EMV2{**
use behavior TestErrorLibrary::simple;

composite error behavior
states
	[sensors.failed or actuator.failed or (control1.failed and control2.failed)]->failed;
--	[control1.failed and control2.failed]->failed;
end composite;
--	properties
--	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;]applies to sensors.Failure;
--  EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to control1.Failure;
--   EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to control2.failure;
--   EMV2::OccurrenceDistribution => [ ProbabilityValue => 0.0000003 ; Distribution => Poisson;] applies to actuator.Failure;
**};

end complete.dual;


device sensor_error extends test_pkg::sensor

annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to Failure;
	**};
end sensor_error;


device actuator_error extends test_pkg::actuator
annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to Failure;
	**};
end actuator_error;

system control_error extends test_pkg::control
annex EMV2{**
    use behavior TestErrorLibrary::simple;
	properties
	EMV2::OccurrenceDistribution => [ ProbabilityValue => 3.0e-7 ; Distribution => Poisson;] applies to Failure;
	**};
end control_error;


end test3_CTMC;

test3_CTMC_complete_dual_Instance__PRISM.pm

ctmc

module complete_dual_instance
	complete_dual_instance_state: [ 0 .. 1] init 0;
endmodule

formula complete_dual_instance_is_operational = complete_dual_instance_state=0;

formula complete_dual_instance_is_failed = complete_dual_instance_state=1;

formula complete_dual_instance_is_failed0 = sensorscomplete_dual_instance_is_failed | actuatorcomplete_dual_instance_is_failed | control1complete_dual_instance_is_failed & control2complete_dual_instance_is_failed;


module sensorscomplete_dual_instance
	sensorscomplete_dual_instance_state: [ 0 .. 1] init 0;
endmodule

formula sensorscomplete_dual_instance_is_operational = sensorscomplete_dual_instance_state=0;

formula sensorscomplete_dual_instance_is_failed = sensorscomplete_dual_instance_state=1;


module actuatorcomplete_dual_instance
	actuatorcomplete_dual_instance_state: [ 0 .. 1] init 0;
	[] actuatorcomplete_dual_instance_state=0 -> 4.0E-4 : (actuatorcomplete_dual_instance_state'=1);
endmodule

formula actuatorcomplete_dual_instance_is_operational = actuatorcomplete_dual_instance_state=0;

formula actuatorcomplete_dual_instance_is_failed = actuatorcomplete_dual_instance_state=1;


module control1complete_dual_instance
	control1complete_dual_instance_state: [ 0 .. 1] init 0;
endmodule

formula control1complete_dual_instance_is_operational = control1complete_dual_instance_state=0;

formula control1complete_dual_instance_is_failed = control1complete_dual_instance_state=1;


module control2complete_dual_instance
	control2complete_dual_instance_state: [ 0 .. 1] init 0;
endmodule

formula control2complete_dual_instance_is_operational = control2complete_dual_instance_state=0;

formula control2complete_dual_instance_is_failed = control2complete_dual_instance_state=1;

test_pkg.aadl

package test_pkg
public

with  ErrorLibrary, EMV2, TestErrorLibrary;
device sensor
features
dpout: out data port;

annex EMV2{**
	use behavior TestErrorLibrary::simple;
properties
EMV2::OccurrenceDistribution => [ ProbabilityValue => 4.0e-4 ; Distribution => Fixed;]
applies to Failed; -- for RBD

**};
end sensor;

device actuator
annex EMV2{**
	use behavior TestErrorLibrary::simple;
properties
-- for RBD
EMV2::OccurrenceDistribution => [ ProbabilityValue => 4.0e-4 ; Distribution => Fixed;] 

applies to Failure;
**};
end actuator;

system control
annex EMV2{**
	use behavior TestErrorLibrary::simple;
properties
-- for RBD
EMV2::OccurrenceDistribution => [ ProbabilityValue => 4.0e-4 ; Distribution => Fixed;]
applies to Failed;

**};
end control;

end test_pkg;

TestErrorLibrary.aadl

package TestErrorLibrary
public
with  ErrorLibrary, EMV2, test_pkg;

annex EMV2 {**
	
	error types extends ErrorLibrary with

No_Flow_Cmd: type extends ServiceOmission;
Bad_Flow_Cmd: type extends BadValue;
Bad_Data: type extends BadValue;
Default_Data: type;

end types;

error behavior Simple
events
Failure: error event;
states
Operational: initial state;
Failed: state;
transitions
BadValueTransition : Operational -[Failure]-> Failed;
end behavior;
	
error behavior three
events
p11: error event;
p12: error event;
p13: error event;
p21: error event;
p22: error event;
p23: error event;
p31: error event;
p32: error event;
p33: error event;
states
nominal: initial state;
bad_data: state;
failed: state;
transitions
tp11: nominal -[p11]-> nominal;
tp12: nominal -[p12]-> bad_data;
tp13: nominal -[p13]-> failed;
--
tp21: bad_data -[p21]-> nominal;
tp22: bad_data -[p22]-> bad_data;
tp23: bad_data -[p23]-> failed;
--
tp31: failed -[p31]-> nominal;
tp32: failed -[p32]-> bad_data;
tp33: failed -[p33]-> failed;
end behavior;
**};
end TestErrorLibrary;