Formal Methods for Embedded Control Software: Some Recent Progress

This contribution introduces key challenges in the verification and validation of industrial-scale embedded control systems, such as those found in the domain of automotive powertrain. Even some of the most basic models of such systems contain features such as nonlinear and hybrid dynamics, which makes the verification problem intractable. A common abstraction for models of such complexity is to treat them as black-box systems, i.e. systems that we can stimulate with a given set of inputs, and can observe the system behaviors for a given set of outputs. We introduce past work that uses a simulation-guided approach for testing and analysis of such black-box models and review some recent progress. We also introduce a logical formalism for specifying behavioral requirements, and review some recent progress on making such requirement formalisms accessible to control designers