Example of MetaH with Reliability Modeling Information
-- This is a triple modular redundant system that uses error masking. This
-- is a common redundancy management approach for aircraft avionics, where
-- very high coverage and very simple software structure is desired, and
-- maintenance is available within a few hours of any failure.
-- This is a basic triple modular redundant system. Three processors host
-- three controllers, and use three busses to communicate with three
-- sensors and three actuators. Each processor votes its inputs to mask
-- errors introduced by a failed sensor or bus. Each actuator votes its
-- inputs to mask errors introduced by a failed processor or bus. Any
-- (covered) single failure is tolerated.
-- Note that this basic model could work with either fail-stop processors
-- (e.g. self-checking pair) or with single processors. With fail-stop
-- processors, the actuator concensus protocols would need to distinguish
-- fail-stop data (in MetaH, look at the .FRESH/.STATUS flag). With
-- fail-stop processors, system failure would occur only when two or more
-- processors failed (self'MaskError for actuators would be 1 ormore, not 2
-- ormore). The system would still fail if more than 1 actuator, sensor or
-- bus failed.
error model Standard is
permanent,
transient: event;
error_free,
unrecoverable,
recoverable: state;
hardware,
software: paths;
end Standard;
error model implementation Standard.NoRecovery is
error_free is initial state;
paths
-- We require that all transition diagrams be fully specified. From
-- every state reachable from the initial state, there must be a
-- transition for every event that might ever occur for the object.
-- The former condition allows a declaration of more states than are
-- actually used for any given class of objects. The latter condition
-- allows an omission of things like propagations from the initial
-- (error_free) state, or fault events that are not declared for a
-- class of objects.
<<hardware>> error_free -[permanent]-> unrecoverable,
error_free -[transient]-> recoverable,
error_free -[recoverable]-> recoverable,
error_free -[unrecoverable]-> unrecoverable,
unrecoverable -[self]-> unrecoverable,
unrecoverable -[permanent]-> unrecoverable,
unrecoverable -[transient]-> unrecoverable,
unrecoverable -[recoverable]-> unrecoverable,
unrecoverable -[unrecoverable]-> unrecoverable,
recoverable -[self]-> error_free,
recoverable -[permanent]-> unrecoverable,
recoverable -[transient]-> recoverable,
recoverable -[recoverable]-> recoverable,
recoverable -[unrecoverable]-> unrecoverable;
<<software>> error_free -[unrecoverable]-> unrecoverable,
error_free -[recoverable]-> recoverable,
unrecoverable -[self]-> unrecoverable,
unrecoverable -[unrecoverable]-> unrecoverable,
unrecoverable -[recoverable]-> unrecoverable,
recoverable -[self]-> recoverable,
recoverable -[unrecoverable]-> unrecoverable,
recoverable -[recoverable]-> recoverable;
end Standard.NoRecovery;
error model implementation Standard.Simple is
error_free is initial state;
paths
<<hardware>> error_free -[permanent]-> unrecoverable,
error_free -[unrecoverable]-> unrecoverable,
unrecoverable -[permanent]-> unrecoverable,
unrecoverable -[unrecoverable]-> unrecoverable,
unrecoverable -[self]-> unrecoverable;
<<software>> error_free -[unrecoverable]-> unrecoverable,
unrecoverable -[unrecoverable]-> unrecoverable,
unrecoverable -[self]-> unrecoverable;
end Standard.Simple;
port type IO_Types is
Sensor_Data_Type: type;
Actuator_Data_Type: type;
end IO_Types;
channel Fiber is
end Fiber;
with port type IO_Types;
device Sensor is
Data: out port IO_Types.Sensor_Data_Type;
Bus: channel Fiber;
end Sensor;
with port type IO_Types;
device Actuator is
Data_1,
Data_2,
Data_3: in port IO_Types.Actuator_Data_Type;
Bus: channel Fiber;
end Actuator;
with error model Standard;
device implementation Actuator.Voting is
attributes
-- Concensus expressions are boolean-valued expressions whose values
-- depend on the error states of the named object. By default, the
-- name of an object evaluates to "true" if it is error-free. In the
-- expression below, names of ports denote the error state of the
-- information being received. There is a syntax to explicitly specify
-- which error states evaluate to "true" for an operand, useful (for
-- example) when some error states are covered and some are not by a
-- particular concensus protocol. In addition to the usual boolean
-- operators 'not' 'and' and 'or', the two operators 'ormore' and
-- 'orless' are available. In this example, errors will not propagate
-- into instances of device Actuator.Voting as long as 2 or more
-- of the received inputs are error-free.
self'MaskError := 2 ormore (Data_1, Data_2, Data_3);
end Actuator.Voting;
with port type IO_Types;
processor Single is
Sensor: out port IO_Types.Sensor_Data_Type;
Actuator: in port IO_Types.Actuator_Data_Type;
Bus_1,
Bus_2,
Bus_3: channel Fiber;
end Single;
with port type IO_Types;
system Multiplex_Computer is
Sensor_1,
Sensor_2,
Sensor_3: out port IO_Types.Sensor_Data_Type;
Actuator_1,
Actuator_2,
Actuator_3: in port IO_Types.Actuator_Data_Type;
end Multiplex_Computer;
-- The Triplex implementation includes separate device
-- components for the sensors and actuators. The
-- system is operable when 2 or more of the actuators
-- are error-free.
with error model Standard;
system implementation Multiplex_Computer.Triplex is
Sensor_A,
Sensor_B,
Sensor_C: device Sensor;
Actuator_A,
Actuator_B,
Actuator_C: device Actuator.Voting;
Computer_A,
Computer_B,
Computer_C: processor Single;
connections
Sensor_1 <- Sensor_A.Data;
Sensor_2 <- Sensor_B.Data;
Sensor_3 <- Sensor_C.Data;
Actuator_A.Data_1 <- Actuator_1;
Actuator_A.Data_2 <- Actuator_2;
Actuator_A.Data_3 <- Actuator_3;
Actuator_B.Data_1 <- Actuator_1;
Actuator_B.Data_2 <- Actuator_2;
Actuator_B.Data_3 <- Actuator_3;
Actuator_C.Data_1 <- Actuator_1;
Actuator_C.Data_2 <- Actuator_2;
Actuator_C.Data_3 <- Actuator_3;
Computer_A.Bus_1 = Sensor_A.Bus;
Computer_A.Bus_2 = Sensor_B.Bus;
Computer_A.Bus_3 = Sensor_C.Bus;
Computer_A.Bus_1 = Actuator_A.Bus;
Computer_A.Bus_2 = Actuator_B.Bus;
Computer_A.Bus_3 = Actuator_C.Bus;
Computer_B.Bus_1 = Sensor_A.Bus;
Computer_B.Bus_2 = Sensor_B.Bus;
Computer_B.Bus_3 = Sensor_C.Bus;
Computer_B.Bus_1 = Actuator_A.Bus;
Computer_B.Bus_2 = Actuator_B.Bus;
Computer_B.Bus_3 = Actuator_C.Bus;
Computer_C.Bus_1 = Sensor_A.Bus;
Computer_C.Bus_2 = Sensor_B.Bus;
Computer_C.Bus_3 = Sensor_C.Bus;
Computer_C.Bus_1 = Actuator_A.Bus;
Computer_C.Bus_2 = Actuator_B.Bus;
Computer_C.Bus_3 = Actuator_C.Bus;
attributes
-- The Poissson arrival rates of the kinds of errors defined in the
-- Standard error model may be set for individual objects. These
-- values could also have been set where a class of objects is defined,
-- e.g. in the Actuator.Voting implementation.
Sensor_A'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Sensor_B'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Sensor_C'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Actuator_A'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Actuator_B'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Actuator_C'FaultEventRate := case (Standard.Permanent => 1.0E-5, Standard.Transient => 1.0E-4);
Computer_A'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Computer_B'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Computer_C'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Sensor_A.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Sensor_B.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Sensor_C.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Actuator_A.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Actuator_B.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Actuator_C.Bus'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
-- The MaskError attribute of a processor models the concensus
-- protocol used by the executive or kernel code, which exchanges state
-- information with kernels hosted on the other processors. Although
-- the executive code is automatically configured by the metah tool,
-- many functions (including the subprogram that implements the
-- concensus protocol) are parameterized and taken from a library. The
-- knowledgable user can easily change the concensus protocol used by
-- the executive/kernel.
Computer_A'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
Computer_B'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
Computer_C'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
self'Operable := 2 ormore (Actuator_A, Actuator_B, Actuator_C);
end Multiplex_Computer.Triplex;
-- The simple implementation includes only the processors.
-- The system is operable when 2 or more of the processors
-- are error-free.
with error model Standard;
system implementation Multiplex_Computer.Simple is
Computer_A,
Computer_B,
Computer_C: processor Single;
connections
<<S1>> Sensor_1 <- Computer_A.Sensor;
<<S2>> Sensor_2 <- Computer_B.Sensor;
<<S3>> Sensor_3 <- Computer_C.Sensor;
<<A1>> Computer_A.Actuator <- Actuator_1;
<<A2>> Computer_B.Actuator <- Actuator_2;
<<A3>> Computer_C.Actuator <- Actuator_3;
Computer_A.Bus_1 = Computer_B.Bus_1;
Computer_A.Bus_1 = Computer_C.Bus_1;
Computer_A.Bus_2 = Computer_B.Bus_2;
Computer_A.Bus_2 = Computer_C.Bus_2;
Computer_A.Bus_3 = Computer_B.Bus_3;
Computer_A.Bus_3 = Computer_C.Bus_3;
attributes
S1'Binding := Computer_A.Bus_1;
S2'Binding := Computer_A.Bus_2;
S3'Binding := Computer_A.Bus_3;
A1'Binding := Computer_A.Bus_1;
A2'Binding := Computer_A.Bus_2;
A3'Binding := Computer_A.Bus_3;
Computer_A'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Computer_B'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Computer_C'FaultEventRate := case (Standard.Permanent => 1.0E-4, Standard.Transient => 1.0E-3);
Computer_A.Bus_1'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Computer_A.Bus_2'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Computer_A.Bus_3'FaultEventRate := case (Standard.Permanent => 1.0E-6, Standard.Transient => 1.0E-4);
Computer_A'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
Computer_B'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
Computer_C'MaskError := 2 ormore (Computer_A, Computer_B, Computer_C);
Computer_A'ClockPeriod := 50 ms;
Computer_B'ClockPeriod := 50 ms;
Computer_C'ClockPeriod := 50 ms;
self'Operable := 2 ormore (Computer_A, Computer_B, Computer_C);
end Multiplex_Computer.Simple;
with port type IO_Types;
process Controller is
Sensor_1,
Sensor_2,
Sensor_3: in port IO_Types.Sensor_Data_Type;
Actuator: out port IO_Types.Actuator_Data_Type;
end Controller;
process implementation Controller.Voting is
attributes
self'MaskError := 2 ormore (Sensor_1, Sensor_2, Sensor_3);
self'Period := 100 ms;
self'SourceTime := 10 ms;
end Controller.Voting;
with port type IO_Types;
macro Multiplex_Controller is
Sensor_1,
Sensor_2,
Sensor_3: in port IO_Types.Sensor_Data_Type;
Actuator_1,
Actuator_2,
Actuator_3: out port IO_Types.Actuator_Data_Type;
end Multiplex_Controller;
macro implementation Multiplex_Controller.Triplex is
Controller_A,
Controller_B,
Controller_C: periodic process Controller.Voting;
connections
<<A1>> Controller_A.Sensor_1 <- Sensor_1;
<<A2>> Controller_A.Sensor_2 <- Sensor_2;
<<A3>> Controller_A.Sensor_3 <- Sensor_3;
<<B1>> Controller_B.Sensor_1 <- Sensor_1;
<<B2>> Controller_B.Sensor_2 <- Sensor_2;
<<B3>> Controller_B.Sensor_3 <- Sensor_3;
<<C1>> Controller_C.Sensor_1 <- Sensor_1;
<<C2>> Controller_C.Sensor_2 <- Sensor_2;
<<C3>> Controller_C.Sensor_3 <- Sensor_3;
<<AA>> Actuator_1 <- Controller_A.Actuator;
<<AB>> Actuator_2 <- Controller_B.Actuator;
<<AC>> Actuator_3 <- Controller_C.Actuator;
attributes
Controller_A'Binding := Computer_A;
Controller_B'Binding := Computer_B;
Controller_C'Binding := Computer_C;
self'Operable := 2 ormore (Controller_A, Controller_B, Controller_C);
end Multiplex_Controller.Triplex;
with error model Standard;
application TMR
is macro Multiplex_Controller.Triplex
on system Multiplex_Computer.Simple; -- alternatively, Multiplex_Computer.Triplex;
connections
<<S1>> Multiplex_Controller.Sensor_1 <- Multiplex_Computer.Sensor_1;
<<S2>> Multiplex_Controller.Sensor_2 <- Multiplex_Computer.Sensor_2;
<<S3>> Multiplex_Controller.Sensor_3 <- Multiplex_Computer.Sensor_3;
<<A1>> Multiplex_Computer.Actuator_1 <- Multiplex_Controller.Actuator_1;
<<A2>> Multiplex_Computer.Actuator_2 <- Multiplex_Controller.Actuator_2;
<<A3>> Multiplex_Computer.Actuator_3 <- Multiplex_Controller.Actuator_3;
attributes
-- The death states are all system states where (not Operable) is true.
-- Both the Multiplex_Controller and the Multiplex_Computer objects
-- have internal 'Operable expressions, and either could be selected
-- here. There are subtle differences, e.g. selecting the software
-- rather than the hardware gives a propagation delay before failure.
-- The complex hardware model specifies the system actually fails
-- when more than one of the actuator devices fails, and these
-- may MaskErrors themselves (eliminating certain transients or
-- bus errors as a cause of failure).
self'Operable := Multiplex_Computer;
-- The simple model is selected here. The current implementation does
-- not implement mechanisms for state space reduction, which would be
-- needed for problems of real-world size.
self'ErrorModel := Standard.Simple;
-- Error paths from the error model define how an object changes error
-- state in response to fault events and error propagations. This form
-- of expressions makes a selection for all components of the application
-- based on the class of the component.
self'ErrorPaths := case (processor => Standard.hardware,
device => Standard.hardware,
channel => Standard.hardware,
memory => Standard.hardware,
process => Standard.software,
monitor => Standard.software,
package => Standard.software,
subprogram => Standard.software,
port => Standard.software);
end TMR;