@inproceedings {157, title = {GPU-based Runtime Verification}, booktitle = {IEEE International Parallel \& Distributed Processing Symposium (IPDPS)}, year = {2013}, month = {May}, abstract = {

Runtime verification is a monitoring technique to gain assurance about well-being of a program at run time. Most existing approaches use sequential monitors; i.e., when the state of the program with respect to an event of interest changes, the monitor interrupts the program execution, evaluates a set of logical properties, and finally resumes the program execution. In this paper, we propose a GPU-based method for design and implementation of monitors that enjoy two levels of parallelism: the monitor (1) works along with the program in parallel, and (2) evaluates a set of properties in a parallel fashion as well. Our parallel monitoring algorithms effectively exploit the many-core platform available in the GPU. In addition to parallel processing, our approach benefits from a true separation of monitoring and functional concerns, as it isolates the monitor in the GPU. Our method is fully implemented and experimental results show significant reduction in monitoring overhead, monitoring interference, and power consumption due to leveraging the GPU technology.

}, keywords = {GPU, Runtime verification}, author = {Shay Berkovich and Borzoo Bonakdarpour and Sebastian Fischmeister} } @inproceedings {76, title = {Time-triggered Program Self-monitoring}, booktitle = {Proc. of 18th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA)}, year = {2012}, pages = {260-269}, address = {Seoul, Korea}, abstract = {

Runtime monitoring aims at analyzing the well-being of a system at run time in order to detect errors and steer the system towards a healthy behavior. Such monitoring is a complementary technique to other approaches for ensuring correctness, such as formal verification and testing. In time-triggered runtime monitoring, a monitor runs as a separate process in parallel with an application program under scrutiny and samples the program\’s state periodically to evaluate a set of properties. Applying this technique in a computing system results in obtaining bounded and predictable overhead. Gaining such characteristics for overhead is highly desirable for designing and engineering time-critical applications, such as safety-critical embedded systems. However, a time-triggered monitor requires certain synchronization features at operating system level and may suffer from various concurrency and synchronization dependencies and overheads as well as possible unreliability of synchronization primitives in a real-time setting. In this paper, we propose a new method, where the program under inspection is instrumented, so that it self-samples its state in a periodic fashion without requiring assistance from an external monitor or internal timer. We call this technique time-triggered self-monitoring. First, we formulate an optimization problem for minimizing the number of points in a program, where self-sampling instrumentation instructions must be inserted. We show that this problem is NP-complete. Consequently, we propose a SAT-based solution and a heuristic to cope with the exponential complexity. Our experimental results show that a time-triggered self-monitored program performs significantly better than the same program monitored by an external time-triggered monitor.

}, keywords = {Runtime verification, TTRV}, doi = {10.1109/RTCSA.2012.16}, author = {Borzoo Bonakdarpour and Johnson Thomas and Sebastian Fischmeister} } @inproceedings {66, title = {Efficient Techniques for Near-optimal Instrumentation in Time-triggered Runtime Verification}, booktitle = {Proc. of the 2nd International Conference on Runtime Verification (RV)}, year = {2011}, month = {September}, pages = {208-222}, address = {San Francisco, USA}, abstract = {

Time-triggered runtime verification aims at tackling two defects associated with runtime overhead normally incurred in event-triggered approaches: unboundedness and unpredictability. In the time-triggered approach, a monitor runs in parallel with the program and periodically samples the program state to evaluate a set of properties. In our previous work, we showed that to increase the sampling period of the monitor (and hence decrease involvement of the monitor), one can employ auxiliary memory to build a history of state changes between subsequent samples. We also showed that the problem of optimization of the size of history and sampling period is NP-complete. In this paper, we propose a set of heuristics that find near-optimal solutions to the problem. Our experiments show that by employing negligible extra memory at run time, we can solve the optimization problem significantly faster, while maintaining a similar level of overhead as the optimal solution. We conclude from our experiments that the NP-completeness of the optimization problem is not an obstacle when applying time-triggered runtime verification in practice.

}, keywords = {Runtime verification, TTRV}, doi = {10.1007/978-3-642-29860-8_16}, url = {http://www.springerlink.com/content/q8812w5u506844u6/}, author = {Samaneh Navabpour and Chun Wah Wallace Wu and Borzoo Bonakdarpour and Fischmeister, Sebastian} } @inproceedings {61, title = {Sampling-based Runtime Verification}, booktitle = {Proceedings of the 17th International Conference on Formal Methods (FM)}, year = {2011}, month = {June}, pages = {88-102}, address = {Limerick, Ireland}, abstract = {

The literature of runtime verification mostly focuses on event-triggered solutions, where a monitor is invoked by every change in the state of the system and evaluates properties of the system. This constant invocation introduces two major drawbacks to the system under scrutiny at run time: (1) significant overhead and (2) unpredictability. To circumvent the latter drawback, in this paper, we introduce a time-triggered approach, where the monitor frequently takes samples from the system to analyze the system\’s health. We propose formal semantics of sampling-based monitoring and discuss how to optimize the sampling period using minimum auxiliary memory. We show that such optimization is NP-complete and consequently introduce a mapping to Integer Linear Programming. Experiments on benchmark applications show that our approach introduces bounded overhead and effectively reduces involvement of the monitor at run time using negligible auxiliary memory.

}, keywords = {monitoring, predictability, Runtime verification, time-triggered}, isbn = {978-3-642-21436-3}, doi = {10.1007/978-3-642-21437-0_9}, url = {http://www.springerlink.com/content/b5304khkjh338720/}, author = {Borzoo Bonakdarpour and Samaneh Navabpour and Fischmeister, Sebastian} }