On-line monitoring for temporal logic robustness

被引：91

作者：

Dokhanchi, Adel ^{[1
]}

Hoxha, Bardh ^{[1
]}

Fainekos, Georgios ^{[1
]}

机构：

[1] School of Computing, Informatics and Decision Systems Engineering, Arizona State University

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8734卷

基金：

美国国家科学基金会;

关键词：

Dynamic programming - Linearization - Embedded systems - Computer circuits - Simulink - Specifications;

D O I：

10.1007/978-3-319-11164-3_19

中图分类号：

学科分类号：

摘要：

In this paper, we provide a Dynamic Programming algorithm for online monitoring of the state robustness of Metric Temporal Logic specifications with past time operators. We compute the robustness of MTL with unbounded past and bounded future temporal operators (MTL<+∞+pt) over sampled traces of Cyber-Physical Systems.We implemented our tool inMatlab as a Simulink block that can be used in any Simulink model. We experimentally demonstrate that the overhead of the MTL<+∞+pt robustness monitoring is acceptable for certain classes of practical specifications. © Springer International Publishing Switzerland 2014.

引用

页码：231 / 246

页数：15

共 30 条

[1]

Alur R., Courcoubetis C., Halbwachs N., Henzinger T.A., Ho P.H., Nicollin X., Olivero A., Sifakis J., Yovine S., The algorithmic analysis of hybrid systems, Theoretical Computer Science, 138, pp. 3-34, (1995)

[2]

Finkbeiner B., Kuhtz L., Monitor circuits for ltl with bounded and unbounded future, RV 2009. LNCS, 5779, pp. 60-75, (2009)

[3]

Havelund K., Rosu G., Monitoring programs using rewriting, Proceedings of the 16th IEEE International Conference on Automated Software Engineering, (2001)

[4]

Havelund K., Rosu G., Synthesizing monitors for safety properties, TACAS 2002. LNCS, 2280, pp. 342-356, (2002)

[5]

Havelund K., Rosu G., Efficient monitoring of safety properties, STTT, 6, pp. 158-173, (2004)

[6]

Kristoffersen K.J., Pedersen C., Andersen H.R., Runtime verification of timed LTL using disjunctive normalized equation systems, Proceedings of the 3rd Workshop on Run-time Verification. ENTCS, 89, pp. 1-16, (2003)

[7]

Maler O., Nickovic D., Monitoring temporal properties of continuous signals, FORMATS/ 2004. LNCS, 3253, pp. 152-166, (2004)

[8]

Reinbacher T., Rozier K.Y., Schumann J., Temporal-logic based runtime observer pairs for system health management of real-time systems, TACAS 2014. LNCS, 8413, pp. 357-372, (2014)

[9]

Rosu G., Havelund K., Synthesizing dynamic programming algorithms from linear temporal logic formulae, (2001)

[10]

Tan L., Kim J., Sokolsky O., Lee I., Model-based testing and monitoring for hybrid embedded systems, Proceedings of the 2004 IEEE International Conference on Information Reuse and Integration, pp. 487-492, (2004)

← 1 2 3 →