Skip to main content
SpringerLink
Log in

Runtime Monitoring for Concurrent Systems

  • Conference paper
  • First Online:
Runtime Verification (RV 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10012))

Included in the following conference series:

Abstract

Most existing specification languages for runtime verification describe the properties of the entire system in a top-down manner, and lack constructs to describe concurrency in the specification directly. \( CSP _E\) is a runtime-monitoring framework based on Hoare’s Communicating Sequential Processes (CSP) that captures concurrency in the specification directly. In this paper, we define the syntax of \( CSP _E\) and its formal semantics. In comparison to quantified event automata (QEA), as an example, \( CSP _E\) describes a specification for a concurrent system in a bottom-up manner, whereas QEA lends itself to a top-down manner. We also present an implementation of \( CSP _E\), which supports full \( CSP _E\) without optimization. When comparing its performance to that of QEA, our implementation of \( CSP _E\) requires slightly more than twice the time required by QEA; we consider this overhead to be acceptable. Finally, we introduce a tool named stracematch, which is developed using \( CSP _E\). It monitors system calls in (Mac) OS X and verifies the usage of file descriptors by a monitored process.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

References

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

    Google Scholar 

  2. Apple: ls, version 7.2.0.0.1.1447826929

    Google Scholar 

  3. Artho, C., Havelund, K., Kumar, R., Yamagata, Y.: Domain-specific languages with Scala. In: Butler, M., et al. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 1–16. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25423-4_1

    Chapter  Google Scholar 

  4. Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from EAGLE to RULER. J. Log. Comput. 20(3), 675–706 (2010). Oxford University Press

    Article  MathSciNet  MATH  Google Scholar 

  5. 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 

  6. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. 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). doi:10.1007/978-3-642-21437-0_7

    Chapter  Google Scholar 

  8. Basin, D., Klaedtke, F., Müller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 1–18. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Bauer, A., Küster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Bauer, A., Falcone, Y.: Decentralised LTL monitoring. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 85–100. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9_10

    Chapter  Google Scholar 

  11. Birchall, C.: ScalaCache. https://github.com/cb372/scalacache

  12. Cantrill, B., Shapiro, M., Leventhal, A.: Dynamic instrumentation of production systems. In: USENIX 2004, pp. 15–22. USENIX (2004)

    Google Scholar 

  13. Cuenca, H.: QEA. https://github.com/selig/qea

  14. Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135–149. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Colombo, C., Pace, G.J., Schneider, G.: LARVA - safer monitoring of real-time Java programs (tool paper). In: Hung, D.V., Krishnan, P. (eds.) SEFM 2009. IEEE Computer Society (2009)

    Google Scholar 

  16. Colombo, C., Francalanza, A., Mizzi, R., Pace, G.J.: polyLarva: runtime verification with configurable resource-aware monitoring boundaries. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 218–232. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  17. D’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. ACM SIGSOFT Softw. Eng. Notes 30(4), 1–7 (2005)

    Article  Google Scholar 

  18. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  19. Drusinsky, D.: Modeling and verification using UML statecharts: a working guide to reactive system design, runtime monitoring and execution-based model checking. Newnes (2011)

    Google Scholar 

  20. Runtime Verification 2014: First international competition on runtime verification. http://rv2014.imag.fr/monitoring-competition/results.html

  21. Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Meth. Syst. Des. 46(3), 226–261 (2014). Springer, US

    Article  MATH  Google Scholar 

  22. Garavel, H., Mateescu, R.: SEQ.OPEN: a tool for efficient trace-based verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 151–157. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  23. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). Springer

    Article  MATH  Google Scholar 

  24. Google Inc.: Chrome, version 47.0.2526.111 (64-bit)

    Google Scholar 

  25. Google Inc.: Guava. https://github.com/google/guava

  26. Goubault-Larrecq, J., Olivain, J.: A smell of Orchids. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 1–20. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. GNU project: bash, version 4.3.42(1)-release (x86_64-apple-darwin14.5.0). https://www.gnu.org/software/bash/

  28. GNU project: Emacs, version 24.5.1. https://www.gnu.org/software/emacs/

  29. GNU project: wget, version 1.17.21-df7cb-dirty built on darwin14.5.0. https://www.gnu.org/software/wget/

  30. Hallé, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192–206 (2012). IEEE

    Article  Google Scholar 

  31. Havelund, K., Roşu, G.: Monitoring programs using rewriting. In: Feather, M., Goedicke, M. (eds.) ASE 2001, pp. 135–143. IEEE CS Press, November 2001

    Google Scholar 

  32. Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) TestCom/FATES 2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  33. Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. 17(2), 143–170 (2014). Springer

    Article  Google Scholar 

  34. Havelund, K., Reger, G.: Specification of parametric monitors: quantified event automata versus rule system. In: Formal Modeling and Verification of Cyber-Physical Systems, pp. 151–189. Springer Fachmedien Wiesbaden (2015)

    Google Scholar 

  35. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International, London (1985)

    MATH  Google Scholar 

  36. Kassem, A., Falcone, Y., Lafourcade, P.: Monitoring electronic exams. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 118–135. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_8

    Chapter  Google Scholar 

  37. Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Arabnia, H.R. (ed.) PDPTA 1999, pp. 279–287. CSREA Press (1999)

    Google Scholar 

  38. Matsumoto, Y.: Ruby, version 2.2.2p95 (2015–04-13 revision 50295) [x86_64-darwin14]

    Google Scholar 

  39. Meredith, P.O., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14(3), 249–289 (2012). Springer

    Article  Google Scholar 

  40. Mizerany, B.: Sinatra, version 1.4.7. http://www.sinatrarb.com/

  41. Odersky, M., Spoon, L., Venners, B.: Programming in Scala. Artima, Suffolk (2016)

    Google Scholar 

  42. Qadeer, S., Tasiran, S.: Runtime verification of concurrency-specific correctness criteria. Int. J. Softw. Tools Technol. Transf. 14(3), 291–305 (2012). Springer

    Article  Google Scholar 

  43. Reger, G.: Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester (2014)

    Google Scholar 

  44. Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596–610. Springer, Heidelberg (2015)

    Google Scholar 

  45. Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)

    Google Scholar 

  46. Stolz, V.: Temporal assertions with parametrized propositions. J. Log. Comput. 20(3), 743–757 (2008). Oxford University Press

    Article  MathSciNet  MATH  Google Scholar 

  47. Stolz, V., Bodden, E.: Temporal assertions using AspectJ. Electron. Notes Theoret. Comput. Sci. 144, 109–124 (2006). Elsevier

    Article  Google Scholar 

  48. Stolz, V., Huch, F.: Runtime verification of concurrent Haskell programs. Electron. Notes Theoret. Comput. Sci. 113, 201–216 (2005). Elsevier

    Article  Google Scholar 

  49. Stucki, N.: multisets. https://github.com/nicolasstucki/multisets

  50. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  51. University of Oxford: FDR3, https://www.cs.ox.ac.uk/projects/fdr/

  52. Yamagata, Y.: CSP_E: log analyzing tool for concurrent systems. https://github.com/yoriyuki/cspe

Download references

Acknowledgments

We are grateful to Giles Reger for helping to develop the QEA models, and to Eijiro Sumii for helping us to develop the proof of Theorem 3. Yoshinao Isobe influenced the early design of the language. This work was supported by JSPS KAKENHI Grant Number JP26280019. We would like to thank Editage (www.editage.jp) for English-language editing.

Author information

Authors and Affiliations

  1. National Institute of Advanced Industrial Science and Technology (AIST), 1-8-31 Midorigaoka, Ikeda, Osaka, 563-8577, Japan

    Yoriyuki Yamagata, Cyrille Artho & Jun Inoue

  2. KTH Royal Institute of Technology, 100 44, Stockholm, Sweden

    Cyrille Artho

  3. The University of Tokyo, 7-3-1 Hongo Bunkyo-ku, Tokyo, 113-8656, Japan

    Masami Hagiya

  4. Chiba University, 1-33 Yayoicho, Inage-ku, Chiba-shi, Chiba, 263-8522, Japan

    Lei Ma & Mitsuharu Yamamoto

  5. Tsurumi University, 2-1-3 Tsurumi, Tsurumi, Yokohama, Kanagawa, 230-0063, Japan

    Yoshinori Tanabe

Authors
  1. Yoriyuki Yamagata
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cyrille Artho
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Masami Hagiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jun Inoue
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Lei Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Yoshinori Tanabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Mitsuharu Yamamoto
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yoriyuki Yamagata .

Editor information

Editors and Affiliations

  1. Université Grenoble Alpes, Inria, Grenoble, France

    Yliès Falcone

  2. IMDEA Software Institute, Madrid, Spain

    César Sánchez

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Yamagata, Y. et al. (2016). Runtime Monitoring for Concurrent Systems. In: Falcone, Y., Sánchez, C. (eds) Runtime Verification. RV 2016. Lecture Notes in Computer Science(), vol 10012. Springer, Cham. https://doi.org/10.1007/978-3-319-46982-9_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46982-9_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46981-2

  • Online ISBN: 978-3-319-46982-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation