Robustness of Specifications and Its Applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo

Georgios Fainekos, Bardh Hoxha, Sriram Sankaranarayanan

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

2 Scopus citations

Abstract

Logical specifications have enabled formal methods by carefully describing what is correct, desired or expected of a given system. They have been widely used in runtime monitoring and applied to domains ranging from medical devices to information security. In this tutorial, we will present the theory and application of robustness of logical specifications. Rather than evaluate logical formulas to Boolean valuations, robustness interpretations attempt to provide numerical valuations that provide degrees of satisfaction, in addition to true/false valuations to models. Such a valuation can help us distinguish between behaviors that “barely” satisfy a specification to those that satisfy it in a robust manner. We will present and compare various notions of robustness in this tutorial, centered primarily around applications to safety-critical Cyber-Physical Systems (CPS). We will also present key ways in which the robustness notions can be applied to problems such as runtime monitoring, falsification search for finding counterexamples, and mining design parameters for synthesis.

Original languageEnglish (US)
Title of host publicationRuntime Verification - 19th International Conference, RV 2019, Proceedings
EditorsBernd Finkbeiner, Leonardo Mariani
PublisherSpringer
Pages27-47
Number of pages21
ISBN (Print)9783030320782
DOIs
StatePublished - 2019
Event19th International Conference on Runtime Verification, RV 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: Oct 8 2019Oct 11 2019

Publication series

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

Conference

Conference19th International Conference on Runtime Verification, RV 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period10/8/1910/11/19

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Robustness of Specifications and Its Applications to Falsification, Parameter Mining, and Runtime Monitoring with S-TaLiRo'. Together they form a unique fingerprint.

Cite this