Reducing Monitoring Overhead by Integrating Event- and Time-Triggered Techniques - Runtime Verification - page 320

(ET) approach, and (2) the time-triggered (TT) method for real-time systems.
We showed that one can effectively exploit the advantages of both approaches
to reduce the overhead of runtime monitoring. To this end, we formulated an
optimization problem that takes into account the cost of different monitoring
interactions (i.e., monitor invocation in ET, sampling and building history in TT,
and mode switching). In particular, the objective of the problem is to minimize
the cumulative overhead in all execution paths using the aforementioned costs.
Since solving the general problem can be computationally unsolvable (e.g., due
to the existence of unbounded loops) or intractable, we proposed a heuristic that
finds suboptimal but effective solutions to the problem by transforming it into an
instance of the integer linear programming problem. Our experimental results on
the SNU-RT benchmark suite showed that our technique effectively reduces the
overhead as compared to selecting the ET or TT method in an ad-hoc manner.
There exist several interesting future research directions. We plan to employ
symbolic execution techniques to implement a more accurate and realistic pre-
diction function used for conditional and loop statements (see Section 3). An-
other open problem is to design other heuristics with lower time complexity that
eliminate subpath generation. Examples include techniques that exploit static
analysis such as graph density and dynamic analysis such as feedback control.
Acknowledgements. This research was supported in part by NSERC Dis-
covery Grant 418396-2012, NSERC Strategic Grant 430575-2012, NSERC DG
357121-2008,ORF-RE03-045, ORF-RE04-036, ORF-RE04-039, CFI 20314, CMC,
and the industrial partners associated with these projects.
References
1. SNU Real-Time Benchmarks,
http://www.cprover.org/goto-cc/examples/snu.html .
2. Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Sampling-based runtime veri-
fication. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 88-102.
Springer, Heidelberg (2011)
3. Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Time-triggered runtime verifi-
cation. Formal Methods in Systems Design (FMSD) 43(1), 29-60 (2013)
4. Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of Temporal Property
Classes. In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 474-486. Springer,
Heidelberg (1992)
5. Colin, S., Mariani, L.: 18 Run-Time Verification. In: Broy, M., Jonsson, B., Katoen,
J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems.
LNCS, vol. 3472, pp. 525-555. Springer, Heidelberg (2005)
6. D'Amorim, M., Rosu, G.: Ecient Monitoring of omega-Languages. In: Etessami,
K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364-378. Springer,
Heidelberg (2005)
7. Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime Verification of Safety-Progress
Properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40-59.
Springer, Heidelberg (2009)