Hybrid cyberphysical system verification with simplex using discrete abstractions

Stanley Bak, Ashley Greer, Sayan Mitra

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 16th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2010
Pages143-152
Number of pages10
DOIs
StatePublished - Jun 28 2010
Event16th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2010 - Stockholm, Sweden
Duration: Apr 12 2010Apr 15 2010

Publication series

NameReal-Time Technology and Applications - Proceedings
ISSN (Print)1080-1812

Other

Other16th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2010
CountrySweden
CityStockholm
Period4/12/104/15/10

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Hybrid cyberphysical system verification with simplex using discrete abstractions'. Together they form a unique fingerprint.

Cite this