Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-physical Systems

Abstract

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.