Monitoring of real-time properties
作者： Andreas Bauer , Martin Leucker , Christian Schallhart
DOI: 10.1007/11944836_25
关键词:
摘要: This paper presents a construction for runtime monitors that check real-time properties expressed in timed LTL (TLTL). Due to D'Souza's results, TLTL can be considered natural extension of towards real-time. Moreover, typical obstacle verification is solved both untimed and formulae, standard models linear temporal logic are infinite traces, whereas only finite system behaviours at hand. Therefore, 3-valued semantics (true, false, inconclusive) on traces defined resembles the trace suitable intuitive manner. Then, describes how construct, given (T)LTL formula, deterministic monitor with three output symbols reads yields its according semantics. Notably, rejects as early possible, any minimal bad prefix results false return value.
springer.com
core.ac.uk
uni-luebeck.de
sci-hub.se 参考文章(28)
Séverine Colin, Leonardo Mariani, 18 Run-Time Verification Model-Based Testing of Reactive Systems. pp. 525- 555 ,(2005) , 10.1007/11498490_24
Grigore Rosu, Marcelo d'Amorim, Efficient Monitoring of omega-Languages. computer aided verification. pp. 364- 378 ,(2005)
Alexander Pretschner, Joost-Pieter Katoen, Manfred Broy, Martin Leucker, Bengt Jonsson, Model-Based Testing of Reactive Systems: Advanced Lectures (Lecture Notes in Computer Science) Springer-Verlag New York, Inc.. ,(2005)
Ravi Sethi, Jeffrey D. Ullman, Alfred V. Aho, Compilers: Principles, Techniques, and Tools ,(1986)
Patricia Bouyer, Fabrice Chevalier, Deepak D’Souza, Fault Diagnosis Using Timed Automata Foundations of Software Science and Computational Structures. pp. 219- 233 ,(2005) , 10.1007/978-3-540-31982-5_14
Stavros Tripakis, Sergio Yovine, Analysis of Timed Systems Using Time-Abstracting Bisimulations formal methods. ,vol. 18, pp. 25- 68 ,(2001) , 10.1023/A:1008734703554
Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata. pp. 238- 266 ,(1996) , 10.1007/3-540-60915-6_6
Stavros Tripakis, Fault Diagnosis for Timed Automata Lecture Notes in Computer Science. pp. 205- 224 ,(2002) , 10.1007/3-540-45739-9_14
Cindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout, Reasoning with Temporal Logic on Truncated Paths computer aided verification. pp. 27- 39 ,(2003) , 10.1007/978-3-540-45069-6_3
Orna Kupferman, Moshe Y. Vardi, Model Checking of Safety Properties formal methods. ,vol. 19, pp. 291- 314 ,(2001) , 10.1023/A:1011254632723