Top

Published in:

2019 | OriginalPaper | Chapter

Testing Equivalence vs. Runtime Monitoring

Authors : Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen

Published in: Models, Languages, and Tools for Concurrent and Distributed Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter An Equational Characterisation of the Must Testing Pre-order for Regular Processes

next chapter Reward Testing Equivalences for Processes

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

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_11CrossRef

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_1CrossRefMATH

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=3290365CrossRef

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

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_9CrossRef

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_82CrossRef

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_4CrossRef

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

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

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.004CrossRef

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.833MathSciNetCrossRefMATH

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.3CrossRef

13.

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

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

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

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_5CrossRef

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

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

19.

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

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.1067MathSciNetCrossRefMATH

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

22.

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

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/030439759090038JMathSciNetCrossRef

24.

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

25.

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

26.

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

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/0304397587901174MathSciNetCrossRef

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

Title: Testing Equivalence vs. Runtime Monitoring
Authors: Luca Aceto
Antonis Achilleos
Adrian Francalanza
Anna Ingólfsdóttir
Karoliina Lehtinen
Publisher: Springer International Publishing
Book: Models, Languages, and Tools for Concurrent and Distributed Programming
Print ISBN: 978-3-030-21484-5

Electronic ISBN: 978-3-030-21485-2

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-21485-2_4

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner