Synthesizing safe control-command systems out of reusable components

•A design method suitable for embedded control systems.•Discrete Controller Synthesis (DCS) for automatic and correct code generation.•Synergy between DCS, formal verification and simulation.•Address questions about controllability, implementation and control validation.

This paper presents a safe design method for control-command embedded systems. It investigates the problem of building control-command systems out of Commercial off the shelf (COTS) components. The design method proposed uses in synergy the formal verification (FV) and the Discrete Controller Synthesis (DCS) techniques. COTS are formally specified using temporal logic and/or executable observers. New functions are built by assembling COTS together. As the COTS assembly operation is seldom error-free, behavioral incompatibilities may persist between COTS. For these reasons, COTS assemblies need to be formally verified and if errors are found, an automatic correction is attempted using DCS. The control-command code generated by DCS needs hardware specific post-processing: a structural decomposition, followed by a controllability assessment, followed by a dedicated formal verification step, ensuring that no spurious behavior is added by DCS. The resulting system is ready for hardware (e.g. FPGA) implementation.