Skip to main content
SpringerLink
Log in
Book cover

International Symposium On Leveraging Applications of Formal Methods, Verification and Validation

ISoLA 2012: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change pp 284–291Cite as

Runtime Verification: The Application Perspective

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7609))

Abstract

In the past decade, Runtime Verification (RV) has gained much focus, from both the research community and practitioners. Roughly speaking, RV combines a set of theories, techniques and tools aiming towards efficient analysis of systems’ executions and guaranteeing their correctness using monitoring techniques. Major challenges in RV include characterizing and formally expressing requirements that can be monitored, proposing intuitive and concise specification formalisms, and monitoring specifications efficiently (time and memory-wise).

With the major strides made in recent years, much effort is still needed to make RV an attractive and viable methodology for industrial use. In addition, further studies are needed to apply RV to wider application domains such as security, bio-health, power micro-grids.

The purpose of the “Runtime Verification: the application perspective” track at ISoLA’12 was to bring together experts on runtime verification and potential application domains to try and advance the state-of-the-art on how to make RV more attractive to industry and usable in additional application domains. This introductory paper proposes an overview of the contributions brought by the papers selected at the track.

The work of the first author was funded in part by the French-government Single Inter-Ministry Fund (FUI) through the IO32 project. The work of the second author was funded in part by NSF award CCF-0916438.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ahrendt, W., Pace, G., Schneider, G.: A unified approach for static and runtime verification: framework and applications. In: Margaria, Steffen [22]

    Google Scholar 

  2. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. In: Johnson, R.E., Gabriel, R.P. (eds.) OOPSLA, pp. 345–364. ACM (2005)

    Google Scholar 

  3. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Barringer, H., Havelund, K.: TraceContract: A Scala DSL for Trace Analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  5. Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675–706 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A., Nouri, A.: Sbip: A statistical model checking extension for BIP. In: Margaria, Steffen [22]

    Google Scholar 

  7. Blech, J.O., Falcone, Y., Rueß, H., Schäetz, B.: Behavioral Specification based Runtime Monitors for OSGi Services. In: Margaria, Steffen [22]

    Google Scholar 

  8. Bodden, E., Hendren, L.J.: The Clara framework for hybrid typestate analysis. STTT 14(3), 307–326 (2012)

    Article  Google Scholar 

  9. Chen, F., Roşu, G.: Parametric Trace Slicing and Monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246–261. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. David, A., Larsen, K.G., Legay, A., Seadwards, S., Poulsen, D.: Systems biology, runtime verification and more. In: Margaria, Steffen [22]

    Google Scholar 

  11. Dimitrova, R., Finkbeiner, B., Rabe, M.: Monitoring temporal information flow. In: Margaria, Steffen [22]

    Google Scholar 

  12. Dormoy, J., Kouchnarenko, O., Lanoix, A.: Using Temporal Logic for Dynamic Reconfigurations of Components. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 200–217. Springer, Heidelberg (2010)

    Google Scholar 

  13. Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime Verification of Component-Based Systems. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 204–220. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Hallé, S., Tremblay-Lessard, R.: A case for “piggyback” runtime monitoring. In: Margaria, Steffen [22]

    Google Scholar 

  15. Hartmanns, A., Hermanns, H.: Modelling and decentralised runtime control of self-stabilising power micro grids. In: Margaria, Steffen [22]

    Google Scholar 

  16. Havelund, K.: What does AI have to do with RV. In: Margaria, Steffen [22]

    Google Scholar 

  17. Havelund, K., Goldberg, A.: Verify Your Runs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 374–383. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Hinrichs, T., Sistla, P.A., Zuck, L.D.: Model checking meets run-time verification. In: Voronkov, A., Korovina, M. (eds.) HOWARD-60: Proceedings of the Higher-Order Workshop on Automated Runtime verification and Debugging (to appear, 2012)

    Google Scholar 

  19. Huang, X., Seyster, J., Callanan, S., Dixit, K., Grosu, R., Smolka, S.A., Stoller, S.D., Zadok, E.: Software monitoring with controllable overhead. STTT 14(3), 327–347 (2012)

    Article  Google Scholar 

  20. Kim, C.H.P., Bodden, E., Batory, D., Khurshid, S.: Reducing Configurations to Monitor in a Software Product Line. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 285–299. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2008)

    Article  Google Scholar 

  22. Margaria, T., Steffen, B.: ISoLA 2012, Part I. LNCS, vol. 7609. Springer, Heidelberg (2012)

    Google Scholar 

  23. Mounier, L., Sifakis, E.: Dynamic information-flow analysis for multi-threaded applications. In: Margaria, Steffen [22]

    Google Scholar 

  24. Pnueli, A., Zaks, A.: PSL Model Checking and Run-Time Verification Via Testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  25. Razavi, N., Holzer, A., Farzan, A.: Bounded-interference sequentialization for testing concurrent programs. In: Margaria, Steffen [22]

    Google Scholar 

  26. Runtime Verification (2001-2012), http://www.runtime-verification.org

  27. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)

    Article  Google Scholar 

  28. Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electr. Notes Theor. Comput. Sci. 144(4), 109–124 (2006)

    Article  Google Scholar 

  29. Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique de Grenoble, University of Grenoble I (UJF), France

    Yliès Falcone

  2. University of Illinois at Chicago, USA

    Lenore D. Zuck

Authors
  1. Yliès Falcone
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lenore D. Zuck
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, Universität Potsdam, August-Bebel-Straße 89, 14482, Potsdam, Germany

    Tiziana Margaria

  2. Fakultät für Informatik, Technische Universität Dortmund, Otto-Hahn-Straße 14, 44227, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Falcone, Y., Zuck, L.D. (2012). Runtime Verification: The Application Perspective. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change. ISoLA 2012. Lecture Notes in Computer Science, vol 7609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34026-0_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-34026-0_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-34025-3

  • Online ISBN: 978-3-642-34026-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation