Formal verification in the loop to enhance verification of safety-critical cyber-physical systems

Formal verification may play a central role in the development of safe controllers, such as those found in electric drives or (semi-)autonomous vehicles, whose complexity arises from the coexistence of mechanical and electrical subsystems with sophisticated electronic controllers that must implement high-level control policies according to different driving modes, while optimizing several objectives, such as safety first and foremost, efficiency, and performance among others. Model-driven development resorts to simulation to assess how well the various requirements and constraints are satisfied, but there is a growing awareness that more rigorous methods are needed to achieve the required levels of safety. This paper proposes a conceptual framework for the development of complex systems based on (i) higher-order logic specification, (ii) verification by theorem proving, and (iii) tight integration of verification with model-driven development and simulation. This framework addresses both digital and analog systems, as illustrated with some examples in different fields including implantable biomedical systems, autonomous vehicles, and electric valve actuation.