Safe design method of embedded control systems Case study

摘要

This paper proposes an approach for safe design of hardware embedded control systems. The approach is based on a combination of formal verification and discrete controller synthesis techniques. Formal verification is solicited to detect design errors and provide counterexamples, while the Discrete Controller Synthesis technique is used to correct those error since it attempts to enforce previously verified specifications which do not hold. It automatically produces control code, which is assembled to the erroneous component in order to provide a system correct by construction with respect to the specification to enforce. We illustrate the approach on a train controller subsystem taken from Bomabardier Transport company.