Verifying cyber-physical interactions in safety-critical systems

Sayan Mitra, Tichakorn Wongpiromsarn, Richard M. Murray

Research output: Contribution to journalArticlepeer-review


Safety-compromising bugs in software-controlled systems are often hard to detect. In a 2007 DARPA Urban Challenge vehicle, such a defect remained hidden during more than 300 miles of test-driving and hours of extensive simulations, manifesting for the first time in a particular physical environment during the competition, which led to a safety violation and its team’s disqualification. With this incident as an example, the authors discuss formalisms and techniques available for safety analysis of cyber-physical systems. They discuss simulation-based approaches, more formal approaches, and the emerging area that attempts to take advantage of both. They highlight these approaches’ merits and limitations and identify open problems, the resolution of which will bolster the development of reliable safety-critical cyber-physical systems.

Original languageEnglish (US)
Article number6531612
Pages (from-to)28-37
Number of pages10
JournalIEEE Security and Privacy
Issue number4
StatePublished - 2013


  • autonomous vehicles
  • formal verification
  • invariant checking
  • simulation-based verification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Electrical and Electronic Engineering
  • Law


Dive into the research topics of 'Verifying cyber-physical interactions in safety-critical systems'. Together they form a unique fingerprint.

Cite this