Robust Online Monitoring of Signal Temporal Logic
Jyotirmoy V. Deshmukhh, Alexandre Donze, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia

Citation
Jyotirmoy V. Deshmukhh, Alexandre Donze, Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. "Robust Online Monitoring of Signal Temporal Logic". Runtime Verification '15, Vienna, 22, September, 2015; Winner of the best paper award.

Abstract
Signal Temporal Logic (STL) is a formalism used to rigorously specify requirements of cyberphysical systems (CPS), i.e., systems mixing digital or discrete components in interaction with a continuous environment or analog components. STL is naturally equipped with a quantitative semantics which can be used for various purposes: from assessing the robustness of a specification to guiding searches over the input and parameter space with the goal of falsifying the given property over system behaviors. Algorithms have been proposed and implemented for offline computation of such quantitative semantics, but only few methods exist for an online setting, where one would want to monitor the satisfaction of a formula during simulation. In this paper, we formalize a semantics for robust online monitoring of partial traces, i.e., traces for which there might not be enough data to decide the Boolean satisfaction (and to compute its quantitative counterpart). We propose an efficient algorithm to compute it and demonstrate its usage on two large scale real-world case studies coming from the automotive domain and from CPS education in a Massively Open Online Course (MOOC) setting. We show that savings in computationally expensive simulations far out- weigh any overheads incurred by an online approach.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Jyotirmoy V. Deshmukhh, Alexandre Donze, Shromona Ghosh,
  Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/571.html">Robust
  Online Monitoring of Signal Temporal Logic</a>,
  Runtime Verification '15, Vienna, 22, September, 2015; <a
  href="http://rv2015.conf.tuwien.ac.at/?page_id=775"
  >Winner of the best paper award</a>.

• Plain text

  Jyotirmoy V. Deshmukhh, Alexandre Donze, Shromona Ghosh,
  Xiaoqing Jin, Garvit Juniwal, Sanjit Seshia. "Robust
  Online Monitoring of Signal Temporal Logic". Runtime
  Verification '15, Vienna, 22, September, 2015; <a
  href="http://rv2015.conf.tuwien.ac.at/?page_id=775"
  >Winner of the best paper award</a>.

• BibTeX

  @inproceedings{DeshmukhhDonzeGhoshJinJuniwalSeshia15_RobustOnlineMonitoringOfSignalTemporalLogic,
      author = {Jyotirmoy V. Deshmukhh and Alexandre Donze and
                Shromona Ghosh and Xiaoqing Jin and Garvit Juniwal
                and Sanjit Seshia},
      title = {Robust Online Monitoring of Signal Temporal Logic},
      booktitle = {Runtime Verification '15, Vienna},
      day = {22},
      month = {September},
      year = {2015},
      note = {<a
                href="http://rv2015.conf.tuwien.ac.at/?page_id=775"
                >Winner of the best paper award</a>.},
      abstract = {Signal Temporal Logic (STL) is a formalism used to
                rigorously specify requirements of cyberphysical
                systems (CPS), i.e., systems mixing digital or
                discrete components in interaction with a
                continuous environment or analog components. STL
                is naturally equipped with a quantitative
                semantics which can be used for various purposes:
                from assessing the robustness of a specification
                to guiding searches over the input and parameter
                space with the goal of falsifying the given
                property over system behaviors. Algorithms have
                been proposed and implemented for offline
                computation of such quantitative semantics, but
                only few methods exist for an online setting,
                where one would want to monitor the satisfaction
                of a formula during simulation. In this paper, we
                formalize a semantics for robust online monitoring
                of partial traces, i.e., traces for which there
                might not be enough data to decide the Boolean
                satisfaction (and to compute its quantitative
                counterpart). We propose an efficient algorithm to
                compute it and demonstrate its usage on two large
                scale real-world case studies coming from the
                automotive domain and from CPS education in a
                Massively Open Online Course (MOOC) setting. We
                show that savings in computationally expensive
                simulations far out- weigh any overheads incurred
                by an online approach. },
      URL = {http://terraswarm.org/pubs/571.html}
  }
  

Posted by Alexandre Donze on 11 May 2015.
Groups: tools