Formal approach for the safety assessment of embedded controller based on programmable electronic hardware

• Method gives assurance when system development or service history data not available.
• Approach shown on embedded control system having legacy components.
• Formal models created from available system description.
• Safety assessment performed using analysis of faulty and non-faulty behaviour.
• Method generates evidence for safety argument and is consistent with known standards.

The issue of providing assurance for programmable electronic hardware (PEH) that have either been previously developed or composed of Commercial-Of-The-Shelf (COTS) and used in embedded control systems is examined. Specifically, these type of PEH are difficult to assure because no evidence may be available on their development and limited functional descriptions may exist to perform a safety assessment. This problem is addressed by presenting a formal approach that allows a safety assessment on a PEH to be performed. This approach uses a system’s architecture and mechanisms such as safety nets to deduce the behaviour of the PEH, which is then translated into the formalism of Petri nets. Since this formalism can be used to model both faulty and non-faulty behaviour, it allows a safety assessment to be performed. Application of this approach is shown via a case study in which a safety assessment is performed for a PEH based embedded controller for an engine control application.