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

Cinzia Bernardeschi, Andrea Domenici, Sergio Saponara


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.

Full Text:




Hosted By Universitätsbibliothek TU Berlin.