Online Parametric Timed Pattern Matching with Automata-Based Skipping

被引：8

作者：

Waga, Masaki ^{[1
,2
]}

Andre, Etienne ^{[1
,3
,4
]}

机构：

[1] Natl Inst Informat, Tokyo, Japan

[2] Sokendai Grad Univ Adv Studies, Hayama, Kanagawa, Japan

[3] Univ Paris 13, LIPN, CNRS, UMR 7030, F-93430 Villetaneuse, France

[4] CNRS, JFLI, Tokyo, Japan

来源：

NASA FORMAL METHODS (NFM 2019) | 2019年 / 11460卷

关键词：

Monitoring; Real-time systems; Parametric timed automata; VERIFICATION;

D O I：

10.1007/978-3-030-20652-9_26

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Timed pattern matching has strong connections with monitoring real-time systems. Given a log and a specification containing timing parameters (that can capture uncertain or unknown constants), parametric timed pattern matching aims at exhibiting for which start and end dates, as well as which parameter valuations, a specification holds on that log. This problem is notably close to robustness. We propose here a new framework for parametric timed pattern matching. Not only we dramatically improve the efficiency when compared to a previous method based on parametric timed model checking, but we further propose optimizations based on skipping. Our algorithm is suitable for online monitoring, and experiments show that it is fast enough to be applied at runtime.

引用

页码：371 / 389

页数：19

共 38 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2]

Alur R., 1993, Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, P592, DOI 10.1145/167088.167242

[3]

Andre Etienne, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P33, DOI 10.1007/978-3-642-32759-9_6

[4] Offline timed pattern matching under uncertainty [J].

Andre, Etienne ;

Hasuo, Ichiro ;

Waga, Masaki .

2018 23RD INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 2018, :10-20

[5] AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA [J].

Andre, Etienne ;

Chatain, Thomas ;

Fribourg, Laurent ;

Encrenaz, Emmanuelle .

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2009, 20 (05) :819-836

[6]

Asarin E., 2012, Runtime Verification: Second International Conference, RV 2011, San Francisco, CA, USA, September 27-30, 2011, Revised Selected Papers 2, V7186, P147, DOI [10.1007/978-3-642-29860-812, 10.1007/978-3-642-29860-8_12, DOI 10.1007/978-3-642-29860-8_12]

[7] Distance on Timed Words and Applications [J].

Asarin, Eugene ;

Basset, Nicolas ;

Degorre, Aldric .

FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2018, 2018, 11022 :199-214

[8] Combining the Temporal and Epistemic Dimensions for MTL Monitoring [J].

Asarin, Eugene ;

Maler, Oded ;

Nickovic, Dejan ;

Ulus, Dogan .

FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2017), 2017, 10419 :207-223

[9] The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems [J].

Bagnara, Roberto ;

Hill, Patricia M. ;

Zaffanella, Enea .

SCIENCE OF COMPUTER PROGRAMMING, 2008, 72 (1-2) :3-21

[10] Efficient Parametric Identification for STL [J].

Bakhirkin, Alexey ;

Ferrere, Thomas ;

Maler, Oded .

HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK), 2018, :177-186

← 1 2 3 4 →