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.
Formal verification in the loop to enhance verification of safety-critical cyber-physical systems
2019-01-01
Article (Journal)
Electronic Resource
English
DDC: | 629 |
Formal Verification of Safety-Critical Aerospace Systems
IEEE | 2023
|Integrated Formal Verification and Validation of Safety Critical Software
British Library Conference Proceedings | 1993
|Formal Verification of Flight Critical Software
AIAA | 2005
|Formal verification of safety requirements on complex systems
Tema Archive | 1996
|Formal Safety Verification of Automotive Microcontroller Parts
Tema Archive | 2012
|