Trace Partitioning and Local Monitoring for Asynchronous Components

  • Duncan Paul AttardEmail author
  • Adrian FrancalanzaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


We propose an instrumentation technique for monitoring asynchronous component systems that departs from the traditional runtime verification set-up assuming a single execution trace. The technique generates partitioned traces that better reflect the interleaved execution of the asynchronous components under scrutiny, and lends itself well to local monitoring. We provide argumentation for the qualitative benefits of our approach, demonstrate its implementability for actor-based systems, and justify claims related to the applicability and efficiency gains via an empirical evaluation over a third party component-based system.


  1. 1.
    Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007)CrossRefGoogle Scholar
  2. 2.
    Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. J. Funct. Program. 7, 1–72 (1997)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (2007)Google Scholar
  4. 4.
    Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473–481. Springer, Cham (2016). doi: 10.1007/978-3-319-46982-9_31CrossRefGoogle Scholar
  5. 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). doi: 10.1007/978-3-642-32759-9_9CrossRefGoogle Scholar
  6. 6.
    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_10CrossRefGoogle Scholar
  7. 7.
    Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38592-6_5CrossRefGoogle Scholar
  8. 8.
    Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176–192. Springer, Cham (2016). doi: 10.1007/978-3-319-33693-0_12CrossRefGoogle Scholar
  9. 9.
    Cesarini, F., Thompson, S.: Erlang Programming. O’Reilly Media, Sebastopol (2009)zbMATHGoogle Scholar
  10. 10.
    Chappell, D.: Enterprise Service Bus: Theory in Practice. O’Reilly Media, Sebastopol (2004)Google Scholar
  11. 11.
    Chen, F., Rosu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246–261. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-00768-2_23CrossRefzbMATHGoogle Scholar
  12. 12.
    Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 140–155. Springer, Cham (2014). doi: 10.1007/978-3-319-11164-3_12CrossRefGoogle Scholar
  13. 13.
    Colombo, C., Francalanza, A., Gatt, R.: Elarva: a monitoring tool for erlang. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 370–374. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-29860-8_29CrossRefGoogle Scholar
  14. 14.
    Falcone, Y., Fernandez, J., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRefGoogle Scholar
  15. 15.
    Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying hennessy-milner logic with recursion at runtime. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 71–86. Springer, Cham (2015). doi: 10.1007/978-3-319-23820-3_5CrossRefGoogle Scholar
  16. 16.
    Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy-Milner Logic with Recursion. Formal Methods Syst. Des., 1–30 (2017)Google Scholar
  17. 17.
    Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. 46(3), 226–261 (2015)CrossRefGoogle Scholar
  18. 18.
    Hebert, F.: Recon. Accessed 13 Mar 2017
  19. 19.
    Hoguin, L.: 99s. Accessed 13 Mar 2017
  20. 20.
    Hohpe, G., Woolf, B.: Enterprise Integration Patterns: Designing, Building, and Deploying Messaging Solutions. Addison-Wesley Professional, Boston (2003)Google Scholar
  21. 21.
    Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: POPL, pp. 582–594. ACM (2016)CrossRefGoogle Scholar
  22. 22.
    Josuttis, N.M.: SOA in Practice: The Art of Distributed System Design: Theory in Practice. O’Reilly Media, Sebastopol (2007)Google Scholar
  23. 23.
    Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265–288 (1990)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)CrossRefGoogle Scholar
  25. 25.
    Safonov, V.O.: Using Aspect-Oriented Programming for Trustworthy Software Development. Wiley-Interscience, Hoboken (2008)CrossRefGoogle Scholar
  26. 26.
    Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: ICSE, pp. 418–427 (2004)Google Scholar
  27. 27.
    Sen, K., Vardhan, A., Agha, G., Rosu, G.: Decentralized runtime analysis of multithreaded applications. In: IPPS (2006)Google Scholar
  28. 28.
    Vella, A., Francalanza, A.: Preliminary results towards contract monitorability. In: PrePost@IFM. EPTCS, vol. 208, pp. 54–63 (2016)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.CS, ICTUniversity of MaltaMsidaMalta

Personalised recommendations