Predictive runtime verification of timed properties

被引：37

作者：

Pinisetty, Srinivas ^{[1
]}

Jeron, Thierry ^{[2
]}

Tripakis, Stavros ^{[1
,3
]}

Falcone, Ylies ^{[4
]}

Marchand, Herve ^{[2
]}

Preoteasa, Viorel ^{[1
]}

机构：

[1] Aalto Univ, Espoo, Finland

[2] INRIA Rennes Bretagne Atlantique, Campus Beaulieu, F-35042 Rennes, France

[3] Univ Calif Berkeley, Berkeley, CA 94720 USA

[4] Univ Grenoble Alpes, INRIA, LIG, F-38000 Grenoble, France

来源：

JOURNAL OF SYSTEMS AND SOFTWARE | 2017年 / 132卷

基金：

美国国家科学基金会; 芬兰科学院;

关键词：

Monitoring; Runtime verification; Timed automata; Real-time systems; ENFORCEMENT;

D O I：

10.1016/j.jss.2017.06.060

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Runtime verification (RV) techniques are used to continuously check whether the (un-trustworthy) output of a black-box system satisfies or violates a desired property. When we consider runtime verification of timed properties, physical time elapsing between actions influences the satisfiability of the property. This paper introduces predictive runtime verification of timed properties where the system is not entirely a black-box but something about its behaviour is known a priori. A priori knowledge about the behaviour of the system allows the verification monitor to foresee the satisfaction (or violation) of the monitored property. In addition to providing a conclusive verdict earlier, the verification monitor also provides additional information such as the minimum (maximum) time when the property can be violated (satisfied) in the future. The feasibility of the proposed approach is demonstrated by a prototype implementation, which is able to synthesize predictive runtime verification monitors from timed automata. (C) 2017 Published by Elsevier Inc.

引用

页码：353 / 365

页数：13

共 42 条

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