Reliable hardware support for the use of formal languages in high assurance systems

A circuit arrangement comprising a series of state machines, the series comprising least a first and a second state machine;

• the first state machine being arranged to have a data output, and an alarm output for indicating incorrect operation, the second state machine being coupled to the data output and the alarm output of the first state machine, and being arranged to verify that the data output and the alarm output of the first state machine are not indicating incorrect operation;
• and
• a last state machine in the series being arranged to output an alarm indicating incorrect operation, and output a data output, the data output being fed back as an input into one of the series of state machines.

A circuit arrangement comprising;

• two or more redundant processing systems, each outputting processed data, and
• a selector for selecting one of the processed data outputs,
• the arrangement further comprising circuitry for checking the correct operation of the respective processing system, the circuitry for checking the processed outputs, and the circuitry for selecting between the processed outputs comprising trusted circuitry, the trusted circuitry comprising circuitry whose design has been proved to be correct, and comprising self-checking circuitry for checking if it has operated incorrectly.

A logic circuit comprising three or more inputs, and the same number of outputs, at least one of the outputs having the same logic value as one of the inputs, another of the outputs having a logic value which is a reversible Boolean function of the three or more inputs, the outputs being reversible such that for any logic values A, B, C, applied to the inputs, if the resulting outputs are reapplied to the inputs, the circuit would regenerate the same logic values of the original inputs A, B, and C.

A verified circuit arrangement comprising:

• a first and a second logic circuit, each comprising a reversible boolean function, coupled in series such that the outputs of the second logic circuit will regenerate the same logic values as the inputs to the first logic circuit, and;
• a comparator arranged to verify the operation of the first logic circuit by comparing the inputs of the first logic circuit with the outputs of the second logic circuit.

A memory arrangement having storage elements, addressable by a content addressing arrangement, an integrity checker for detecting faulty storage elements, and

• an arrangement for turning off storage elements found to be faulty during operation, while maintaining availability of the remaining storage elements.