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 language | English |
---|---|
Title of host publication | Runtime Verification |
Subtitle of host publication | 20th International Conference, RV 2020, Los Angeles, CA, USA, October 6–9, 2020, Proceedings |
Publisher | Springer |
Pages | 339–358 |
Number of pages | 20 |
ISBN (Electronic) | 978-3-030-60508-7 |
ISBN (Print) | 978-3-030-60507-0 |
DOIs | |
Publication status | Published - 2 Oct 2020 |
Event | 20th International Conference on Runtime Verification - Virtual Conference Duration: 6 Oct 2020 → 9 Oct 2020 https://rv20.ait.ac.at/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 12399 |
ISSN (Print) | 1611-3349 |
ISSN (Electronic) | 0302-9743 |
Conference
Conference | 20th International Conference on Runtime Verification |
---|---|
Abbreviated title | RV 2020 |
City | Virtual Conference |
Period | 6/10/20 → 9/10/20 |
Internet address |