Safe Environmental Envelopes of Discrete Systems

Rômulo Meira-Góes, Ian Dardik, Eunsuk Kang, Stéphane Lafortune, Stavros Tripakis

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

Abstract

A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is robust against environmental deviations. This paper proposes a notion of robustness as an explicit, first-class property of a transition system that captures how robust it is against possible deviations in the environment. We modeled deviations as a set of transitions that may be added to the original environment. Our robustness notion then describes the safety envelope of this system, i.e., it captures all sets of extra environment transitions for which the system still guarantees a desired property. We show that being able to explicitly reason about robustness enables new types of system analysis and design tasks beyond the common verification problem stated above. We demonstrate the application of our framework on case studies involving a radiation therapy interface, an electronic voting machine, a fare collection protocol, and a medical pump device.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 35th International Conference, CAV 2023, Proceedings
EditorsConstantin Enea, Akash Lal
PublisherSpringer Science and Business Media Deutschland GmbH
Pages326-350
Number of pages25
ISBN (Print)9783031377051
DOIs
StatePublished - 2023
Event35th International Conference on Computer Aided Verification, CAV 2023 - Paris, France
Duration: Jul 17 2023Jul 22 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13964 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference35th International Conference on Computer Aided Verification, CAV 2023
Country/TerritoryFrance
CityParis
Period7/17/237/22/23

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Cite this