Time-triggered Runtime Verification

Time-triggered runtime verification aims to maximize predictability of the monitoring systems and thus tries to enable an engineerable solution for runtime monitoring.

Runtime verification is a formal technique used to check whether a program under inspection satisfies its specification by using a runtime monitor. The monitor traditionally uses one of two ways for evaluating a set of logical properties: (1) event-triggered, where the monitor is triggered when the state of the program changes, and (2) time-triggered, where a monitor periodically reads the state of the program. Realizing the former is straightforward, but the runtime behaviour of event-triggered monitors are difficult to predict. Time-triggerd monitoring, on the other hand, provides predictable monitoring behaviour and strict overhead bounds at run time. 

Project members: 
Last updated: July 18, 2014

Related Publications

Navabpour, S., C. Wah Wallac Wu, B. Bonakdarpour, and S. Fischmeister, "Efficient Techniques for Near-optimal Instrumentation in Time-triggered Runtime Verification", Proc. of the 2nd International Conference on Runtime Verification (RV), San Francisco, USA, pp. 208-222, September, 2011. PDF icon [paper] (433.08 KB)
Navabpour, S., B. Bonakdarpour, and S. Fischmeister, "Optimal Instrumentation of Data-flow in Concurrent Data Structures", Proc. of the 15th International Conference On Principles Of Distributed Systems (OPODIS), Toulouse, France, pp. 497-512, December, 2011. PDF icon [paper] (417.18 KB)
Bonakdarpour, B., and S. Fischmeister, "Runtime Monitoring of Time-sensitive Systems --- Tutorial Supplement", Proc. of the 2nd International Conference on Runtime Verification (RV), San Francisco, USA, 2011. PDF icon [tutorial] (1.28 MB)
Bonakdarpour, B., S. Navabpour, and S. Fischmeister, "Sampling-based Runtime Verification", Proceedings of the 17th International Conference on Formal Methods (FM), Limerick, Ireland, pp. 88-102, June, 2011. PDF icon [paper] (1.45 MB)