Article

polyLARVA: runtime verification with configurable resource-aware monitoring boundaries

Authors:

Christian Colombo,

Adrian Francalanza,

Ruth Mizzi,

Gordon J. PaceAuthors Info & Claims

SEFM'12: Proceedings of the 10th international conference on Software Engineering and Formal Methods

Pages 218 - 232

https://doi.org/10.1007/978-3-642-33826-7_15

Published: 01 October 2012 Publication History

Publisher Site

Abstract

Runtime verification techniques are increasingly being applied in industry as a lightweight formal approach to achieve added assurance of correctness at runtime. A key issue determining the adoption of these techniques is the overheads introduced by the runtime checks, affecting the performances of the monitored systems. Despite advancements in the development of optimisation techniques lowering these overheads, industrial settings such as online portals present new challenges, since they frequently involve the handling of high volume transaction throughputs and cannot afford substantial deterioration in the service they provide.

One approach to reduce overheads is the deployment of the verification computation on auxiliary computing resources, creating a boundary between the system and the verification code. This limits the use of system resources with resource intensive verification being carried out on the remote-side. However, under particular scenarios this approach may still not be ideal, as it may induce significant communication overheads. In this paper, we propose a framework which enables fine-tuning of the tradeoff between processing, memory and communication monitoring overheads, through the use of a user-configurable monitoring boundary. This approach has been implemented in the second generation of the Larva runtime verification tool, poly Larva.

References

[1]

Arnold, M., Vechev, M., Yahav, E.: Qvm: an efficient runtime for detecting defects in deployed systems. SIGPLAN Not. 43, 143-162 (2008).

Digital Library

Google Scholar

[2]

Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Rosu, G., Sokolsky, O., Tillmann, N. (eds.): RV 2010. LNCS, vol. 6418. Springer, Heidelberg (2010).

Google Scholar

[3]

Bodden, E., Chen, F., Rosu, G.: Dependent advice: a general approach to optimizing history-based aspects. In: Proceedings of the 8th ACM International Conference on Aspect-Oriented Software Development, AOSD 2009, pp. 3-14. ACM (2009).

Digital Library

Google Scholar

[4]

Bodden, E., Hendren, L., Lhoták, O.: A Staged Static Program Analysis to Improve the Performance of Runtime Monitoring. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 525-549. Springer, Heidelberg (2007).

Digital Library

Google Scholar

[5]

Colombo, C., Pace, G.J., Schneider, G.: Larva--safer monitoring of real-time java programs (tool paper). In: Seventh IEEE International Conference on Software Engineering and Formal Methods (SEFM), pp. 33-37. IEEE (2009).

Digital Library

Google Scholar

[6]

Dwyer, M.B., Diep, M., Elbaum, S.: Reducing the cost of path property monitoring through sampling. In: Proceedings of the 2008 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE 2008, pp. 228-237. IEEE (2008).

Digital Library

Google Scholar

[7]

Geilen, M.: On the construction of monitors for temporal logic properties. Electr. Notes Theor. Comput. Sci. 55(2), 181-199 (2001).

Google Scholar

[8]

Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-mac: A run-time assurance approach for java programs. Formal Methods in System Design 24, 129-155 (2004).

Digital Library

Google Scholar

[9]

Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. International Journal on Software Techniques for Technology Transfer (2011) (to appear).

Digital Library

Google Scholar

[10]

Sen, K., Rosu, G., Agha, G.: Generating Optimal Linear Temporal Logic Monitors by Coinduction. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 260-275. Springer, Heidelberg (2003).

Google Scholar

Cited By

View all

Shafiei NHavelund KMehlitz P(2023)Concurrent runtime verification of data rich eventsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00713-225:4(481-501)Online publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1007/s10009-023-00713-2
Shafiei NHavelund KMehlitz P(2020)Actor-Based Runtime Verification with MESARuntime Verification10.1007/978-3-030-60508-7_12(221-240)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-60508-7_12
Zhang TEakman GLee ISokolsky O(2019)Overhead-Aware Deployment of Runtime MonitorsRuntime Verification10.1007/978-3-030-32079-9_22(375-381)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_22
Show More Cited By

Recommendations

Efficient Java exception handling in just-in-time compilation
Research Articles

Java uses exceptions to provide elegant error handling capabilities during program execution. However, the presence of exception handlers complicates the job of the just-in-time (JIT) compiler, while exceptions are rarely used in most programs. This ...
Exception Handling during Asynchronous Method Invocation (Research Note)
Euro-Par '02: Proceedings of the 8th International Euro-Par Conference on Parallel Processing

Exception handling mechanisms provided by sequential programming languages rely upon the call stack for the propagation of exceptions. Unfortunately, this is inadequate for handling exceptions thrown from asynchronously invoked methods. For instance, ...
Collaborative Runtime Verification with Tracematches

Perfect pre-deployment test coverage is notoriously difficult to achieve for large applications. Given enough end users, however, many more test cases will be encountered during an application's deployment than during testing. The use of runtime ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SEFM'12: Proceedings of the 10th international conference on Software Engineering and Formal Methods

October 2012

383 pages

ISBN:9783642338250

Editors:
George Eleftherakis
Internal Faculty, CITY College, Computer Science Department, The University of Sheffield, 3 Leontos Sofou St., 546 26, Thessaloniki, Greece
,
Mike Hinchey
Lero - the Irish Software Engineering Research Centre, University of Limerick, 3 Leontos Sofou St., 546 26, Limerick, Ireland
,
Mike Holcombe
Department of Computer Science, Regent Court, 211 Portobello, University of Sheffield, 3 Leontos Sofou St., 546 26, S1 4DP, UK

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 October 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 04 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Shafiei NHavelund KMehlitz P(2023)Concurrent runtime verification of data rich eventsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00713-225:4(481-501)Online publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1007/s10009-023-00713-2
Shafiei NHavelund KMehlitz P(2020)Actor-Based Runtime Verification with MESARuntime Verification10.1007/978-3-030-60508-7_12(221-240)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-60508-7_12
Zhang TEakman GLee ISokolsky O(2019)Overhead-Aware Deployment of Runtime MonitorsRuntime Verification10.1007/978-3-030-32079-9_22(375-381)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32079-9_22
Cassar IFrancalanza A(2016)On Implementing a Monitor-Oriented Programming Framework for Actor SystemsProceedings of the 12th International Conference on Integrated Formal Methods - Volume 968110.1007/978-3-319-33693-0_12(176-192)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-33693-0_12

Abstract

References

Cited By

Recommendations

Efficient Java exception handling in just-in-time compilation

Exception Handling during Asynchronous Method Invocation (Research Note)

Collaborative Runtime Verification with Tracematches

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations