Hybrid Cyberphysical System Verification with Simplex Using Discrete Abstractions

Providing integrity, efficiency, and performance guarantees is a key challenge in the development of next-generation cyberphysical systems. Rather than mandating complete system verification, the Simplex Architecture provides robust designs by incorporating a supervisory controller that takes corrective action only when the system is in danger of violating a desired invariant property such as safety. The central issue in applying this approach is designing the switching logic for the supervisory controller such that it guarantees safety and at the same time is not overly conservative.Previous research in the area relied on finding Lyapunov functions for the underlying continuous dynamical system. In contrast, in this paper, we present an automatic method for solving this design problem through discrete abstractions of the underlying hybrid system and model checking. We present a case study where, in collaboration with John Deere, we use the developed approach to create the Simplex decision module for an off-road vehicle, which is formally verified as both correct and timely.