Skip to main content
SpringerLink
Log in
Book cover

Models, Languages, and Tools for Concurrent and Distributed Programming pp 28–44Cite as

Testing Equivalence vs. Runtime Monitoring

  • Chapter
  • First Online:

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

Abstract

Rocco De Nicola’s most cited paper, which was coauthored with his PhD supervisor Matthew Hennessy, introduced three seminal testing equivalences over processes represented as states in labelled transition systems. This article relates those classic process semantics with the framework for runtime monitoring developed by the authors in the context of the project ‘TheoFoMon: Theoretical Foundations for Monitorability’. It shows that may-testing semantics is closely related to the basic monitoring set-up within that framework, whereas, over strongly-convergent processes, must-testing semantics is induced by a collection of monitors that can detect when processes are unable to perform certain actions.

This research was partially supported by the projects ‘TheoFoMon: Theoretical Foundations for Monitorability’ (grant number: 163406-051; http://icetcs.ru.is/theofomon/) and ‘Epistemic Logic for Distributed Runtime Monitoring’ (grant number: 184940-051) of the Icelandic Research Fund, by the BMBF project ‘Aramis II’ (project number: 01IS160253) and the EPSRC project ‘Solving parity games in theory and practice’ (project number: EP/P020909/1).

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

Learn about institutional subscriptions

Notes

  1. 1.

    Source: https://scholar.google.com/citations?user=Meb6JFkAAAAJ&hl=en, last accessed on the 24th of March 2019.

References

  1. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 203–220. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_11

    Chapter  Google Scholar 

  2. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: On the complexity of determinizing monitors. In: Carayol, A., Nicaud, C. (eds.) CIAA 2017. LNCS, vol. 10329, pp. 1–13. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60134-2_1

    Chapter  MATH  Google Scholar 

  3. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. In: Proceedings of the ACM on Programming Languages (POPL), vol. 3, pp. 52:1–52:29 (2019). https://dl.acm.org/citation.cfm?id=3290365

    Article  Google Scholar 

  4. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: The cost of monitoring alone. CoRR abs/1902.05152 (2019). http://arxiv.org/abs/1902.05152

  5. Aceto, L., De Nicola, R., Fantechi, A.: Testing equivalences for event structures. In: Zilli, M.V. (ed.) Mathematical Models for the Semantics of Parallelism. LNCS, vol. 280, pp. 1–20. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-18419-8_9

    Chapter  Google Scholar 

  6. Aceto, L., Ingólfsdóttir, A.: A theory of testing for ACP. In: Baeten, J.C.M., Groote, J.F. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 78–95. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-54430-5_82

    Chapter  Google Scholar 

  7. Aceto, L., Ingólfsdóttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FoSSaCS 1999. LNCS, vol. 1578, pp. 41–55. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49019-1_4

    Chapter  Google Scholar 

  8. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, New York (2007). https://doi.org/10.1017/cbo9780511814105

    Book  MATH  Google Scholar 

  9. Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification - Introductory and Advanced Topics. LNCS, vol. 10457. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5

    Book  Google Scholar 

  10. Bernardi, G.T., Francalanza, A.: Full-abstraction for client testing preorders. Sci. Comput. Program. 168, 94–117 (2018). https://doi.org/10.1016/j.scico.2018.08.004

    Article  Google Scholar 

  11. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984). https://doi.org/10.1145/828.833

    Article  MathSciNet  MATH  Google Scholar 

  12. Cerone, A., Hennessy, M.: Process behaviour: formulae vs. tests (extended abstract). In: Fröschle, S.B., Valencia, F.D. (eds.) Proceedings 17th International Workshop on Expressiveness in Concurrency, EXPRESS 2010. Electronic Proceedings in Theoretical Computer Science, vol. 41, pp. 31–45 (2010). https://doi.org/10.4204/EPTCS.41.3

    Article  Google Scholar 

  13. De Nicola, R.: Extensional equivalences for transition systems. Acta Informatica 24(2), 211–237 (1987). https://doi.org/10.1007/BF00264365

    Article  MathSciNet  MATH  Google Scholar 

  14. de Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. In: Diaz, Josep (ed.) ICALP 1983. LNCS, vol. 154, pp. 548–560. Springer, Heidelberg (1983). https://doi.org/10.1007/BFb0036936

    Chapter  Google Scholar 

  15. De Nicola, R., Hennessy, M.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83–133 (1984). https://doi.org/10.1016/0304-3975(84)90113-0

    Article  MathSciNet  MATH  Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-319-23820-3_5

    Chapter  Google Scholar 

  17. Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the Hennessy-Milner logic with recursion. Form. Methods Syst. Des. 51(1), 87–116 (2017). https://doi.org/10.1007/s10703-017-0273-z

    Article  MATH  Google Scholar 

  18. van Glabbeek, R.J.: The linear time - branching time spectrum I: the semantics of concrete, sequential processes (Chap. 1). In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  19. Hennessy, M.: Algebraic Theory of Processes. Foundations of Computing, MIT Press, Cambridge (1988)

    MATH  Google Scholar 

  20. Hennessy, M., Ingolfsdottir, A.: A theory of communicating processes with value passing. Inf. Comput. 107(2), 202–236 (1993). https://doi.org/10.1006/inco.1993.1067

    Article  MathSciNet  MATH  Google Scholar 

  21. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990). https://doi.org/10.1016/0890-5401(90)90025-D

    Article  MathSciNet  MATH  Google Scholar 

  22. Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976). https://doi.org/10.1145/360248.360251

    Article  MathSciNet  MATH  Google Scholar 

  23. Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. Theor. Comput. Sci. 72(2), 265–288 (1990). https://doi.org/10.1016/0304-3975(90)90038-J. http://www.sciencedirect.com/science/article/pii/030439759090038J

    Article  MathSciNet  Google Scholar 

  24. Loemker, L.E. (ed.): G. W. Leibniz: Philosophical Papers and Letters, 2nd edn. D. Reidel, Dordrecht (1969)

    Google Scholar 

  25. Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3

    Book  MATH  Google Scholar 

  26. Morris, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (1968)

    Google Scholar 

  27. Phillips, I.: Refusal testing. Theor. Comput. Sci. 50(3),241–284 (1987). https://doi.org/10.1016/0304-3975(87)90117-4. http://www.sciencedirect.com/science/article/pii/0304397587901174

    Article  MathSciNet  Google Scholar 

  28. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Aho, A.V., et al. (eds.) Proceedings of the 5th Annual ACM Symposium on Theory of Computing, pp. 1–9. ACM (1973). https://doi.org/10.1145/800125.804029

  29. Winskel, G.: Synchronization trees. Theor. Comput. Sci. 34, 33–82 (1984). https://doi.org/10.1016/0304-3975(84)90112-9

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

We are grateful to the anonymous reviewers for their suggestions, which helped us to improve the paper. Luca Aceto thanks Ugo Montanari, who asked him a question that led to the work presented in this article during a talk he gave at IMT Lucca in July 2018. Luca Aceto and Anna Ingólfsdóttir have been lucky to count Rocco De Nicola as one of their friends and mentors for many years. Luca Aceto’s ‘tesi di laurea’ was jointly supervised by Rocco De Nicola and Alessandro Fantechi, and he was one of the first two students to graduate under Rocco De Nicola’s supervision in 1986.

Author information

Authors and Affiliations

  1. Gran Sasso Science Institute, L’Aquila, Italy

    Luca Aceto

  2. School of Computer Science, Reykjavik University, Reykjavik, Iceland

    Luca Aceto, Antonis Achilleos & Anna Ingólfsdóttir

  3. Department of Computer Science, ICT, University of Malta, Msida, Malta

    Adrian Francalanza

  4. Department of Computer Science, University of Liverpool, Liverpool, UK

    Karoliina Lehtinen

Authors
  1. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antonis Achilleos
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Anna Ingólfsdóttir
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Karoliina Lehtinen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Aceto .

Editor information

Editors and Affiliations

  1. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

    Michele Boreale

  2. School of Science and Technology, University of Camerino, Camerino, Italy

    Flavio Corradini

  3. School of Science and Technology, University of Camerino, Camerino, Italy

    Michele Loreti

  4. Department of Statistics, Computer Science, Applications, University of Florence, Florence, Italy

    Rosario Pugliese

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K. (2019). Testing Equivalence vs. Runtime Monitoring. In: Boreale, M., Corradini, F., Loreti, M., Pugliese, R. (eds) Models, Languages, and Tools for Concurrent and Distributed Programming. Lecture Notes in Computer Science(), vol 11665. Springer, Cham. https://doi.org/10.1007/978-3-030-21485-2_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21485-2_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21484-5

  • Online ISBN: 978-3-030-21485-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation