Property-Directed Verified Monitoring of Signal Temporal Logic

Ian Stark, Thomas Wright

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

Abstract

Signal Temporal Logic monitoring over numerical simulation traces has emerged as an effective approach to approximate verification of continuous and hybrid systems. In this paper we explore an exact verification procedure for STL properties based on monitoring verified traces in the form of Taylor model flowpipes as produced by the Flow* verified integrator. We explore how tight integration with Flow*’s symbolic flowpipe representation can lead to more precise and more efficient monitoring. We then show how the performance of monitoring can be increased substantially by introducing masks, a property-directed refinement of our method which restricts flowpipe monitoring to the time regions relevant to the overall truth of a complex proposition. Finally, we apply our implementation of these methods to verifying properties of a challenging continuous system, evaluating the impact of each aspect of our procedure on monitoring performance.
Original languageEnglish
Title of host publicationRuntime Verification
Subtitle of host publication20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings
PublisherSpringer
Pages339–358
Number of pages20
ISBN (Electronic)978-3-030-60508-7
ISBN (Print)978-3-030-60507-0
DOIs
Publication statusPublished - 2 Oct 2020
Event20th International Conference on Runtime Verification - Virtual Conference
Duration: 6 Oct 20209 Oct 2020
https://rv20.ait.ac.at/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12399
ISSN (Print)1611-3349
ISSN (Electronic)0302-9743

Conference

Conference20th International Conference on Runtime Verification
Abbreviated titleRV 2020
CityVirtual Conference
Period6/10/209/10/20
Internet address

Fingerprint

Dive into the research topics of 'Property-Directed Verified Monitoring of Signal Temporal Logic'. Together they form a unique fingerprint.

Cite this