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
For additional information, see the Publications FAQ or contact webmaster at terraswarm org.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.