Timed Büchi automata provide a very expressive formalism for expressing requirements of real-time systems. Online monitoring of embedded real-time systems can then be achieved by symbolic execution of such automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring algorithm, which handles such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata. We have implemented our monitoring algorithm on top of the real-time model checking tool Uppaal, and report on encouraging initial results.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Monitoring Real-Time Systems Under Parametric Delay

  • Martin Fränzle,
  • Thomas M. Grosen,
  • Kim G. Larsen,
  • Martin Zimmermann

摘要

Timed Büchi automata provide a very expressive formalism for expressing requirements of real-time systems. Online monitoring of embedded real-time systems can then be achieved by symbolic execution of such automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring algorithm, which handles such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata. We have implemented our monitoring algorithm on top of the real-time model checking tool Uppaal, and report on encouraging initial results.