×

zbMATH — the first resource for mathematics

Monitoring networks through multiparty session types. (English) Zbl 1359.68215
Summary: In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored \(\pi\)-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
KLAIM; Scribble; SPY
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aktug, I.; Dam, M.; Gurov, D., Provably correct runtime monitoring, J. Log. Algebr. Program., 78, 5, 304-339, (2009) · Zbl 1192.68116
[2] Ancona, D.; Drossopoulou, S.; Mascardi, V., Automatic generation of self-monitoring MASs from multiparty global session types in jason, (DALT, Lecture Notes in Comput. Sci., vol. 7784, (2012), Springer), 1-17
[3] Anderson, G.; Rathke, J., Dynamic software update for message passing programs, (APLAS, Lecture Notes in Comput. Sci., vol. 7705, (2012), Springer), 207-222
[4] Baresi, L.; Ghezzi, C.; Guinea, S., Smart monitors for composed services, (ICSOC, (2004), ACM), 193-202
[5] Baresi, L.; Guinea, S.; Pistore, M.; Trainotti, M., Dynamo + astro: an integrated approach for BPEL monitoring, (2009 IEEE International Conference on Web Services, (2009)), 230-237
[6] Bettini, L.; Coppo, M.; D’Antoni, L.; Luca, M. D.; Dezani-Ciancaglini, M.; Yoshida, N., Global progress in dynamically interleaved multiparty sessions, (CONCUR, Lecture Notes in Comput. Sci., vol. 5201, (2008), Springer), 418-433 · Zbl 1160.68456
[7] Bocchi, L.; Chen, T.-C.; Demangeon, R.; Honda, K.; Yoshida, N., Monitoring networks through multiparty session types, (FMOODS/FORTE, Lecture Notes in Comput. Sci., vol. 7892, (2013), Springer), 50-65
[8] Bocchi, L.; Demangeon, R.; Yoshida, N., A multiparty multi-session logic, (TGC, Lecture Notes in Comput. Sci., vol. 8191, (2012), Springer), 97-111
[9] Bocchi, L.; Honda, K.; Tuosto, E.; Yoshida, N., A theory of design-by-contract for distributed multiparty interactions, (CONCUR, Lecture Notes in Comput. Sci., vol. 6269, (2010), Springer), 162-176 · Zbl 1287.68121
[10] Bocchi, L.; Yang, W.; Yoshida, N., Timed multiparty session types, (CONCUR, Lecture Notes in Comput. Sci., vol. 8704, (2014), Springer), 419-434 · Zbl 1417.68117
[11] Cambronero, M.-E., Validation and verification of web services choreographies by using timed automata, J. Log. Algebr. Program., 80, 1, 25-49, (2011) · Zbl 1207.68082
[12] Capecchi, S.; Castellani, I.; Dezani-Ciancaglini, M., Information flow safety in multiparty sessions, (EXPRESS, Electron. Proc. Theor. Comput. Sci., vol. 64, (2011)), 16-30
[13] Capecchi, S.; Giachino, E.; Yoshida, N., Global escape in multiparty session, (FSTTCS, LIPIcs. Leibniz Int. Proc. Inform., vol. 8, (2010), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 338-351 · Zbl 1245.68019
[14] Chen, F.; Rosu, G., MOP: an efficient and generic runtime verification framework, (OOPSLA, (2007), ACM), 569-588
[15] Chen, T.; Honda, K., Specifying stateful asynchronous properties for distributed programs, (CONCUR, Lecture Notes in Comput. Sci., vol. 7454, (2012), Springer), 209-224 · Zbl 1364.68279
[16] Chen, T.-C., Theories for session-based governance for large-scale distributed systems, (2013), Queen Mary, University of London, PhD thesis
[17] Chen, T.-C.; Bocchi, L.; Deniélou, P.-M.; Honda, K.; Yoshida, N., Asynchronous distributed monitoring for multiparty session enforcement, (TGC, Lecture Notes in Comput. Sci., vol. 7173, (2011), Springer), 25-45
[18] Coppo, M.; Dezani-Ciancaglini, M.; Venneri, B., Self-adaptive monitors for multiparty sessions, (PDP, (2014), IEEE), 688-696
[19] De Nicola, R.; Ferrari, G.; Pugliese, R., Klaim: a kernel language for agents interaction and mobility, IEEE Trans. Softw. Eng., 24, 315-330, (1998)
[20] Demangeon, R.; Honda, K., Nested protocols in session types, (CONCUR, Lecture Notes in Comput. Sci., vol. 7454, (2012), Springer), 272-286 · Zbl 1364.68281
[21] Demangeon, R.; Honda, K.; Hu, R.; Neykova, R.; Yoshida, N., Practical interruptible conversations: distributed dynamic verification with multiparty session types and python, Form. Methods Syst. Des., 1-29, (2015) · Zbl 1341.68118
[22] Demangeon, R.; Yoshida, N., On the expressiveness of multiparty sessions, (FSTTCS, LIPIcs. Leibniz Int. Proc. Inform., vol. 45, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 560-574 · Zbl 1366.68012
[23] Deniélou, P.-M.; Yoshida, N., Dynamic multirole session types, (POPL, (2011), ACM), 435-446 · Zbl 1284.68049
[24] Deniélou, P.-M.; Yoshida, N., Multiparty session types meet communicating automata, (ESOP, Lecture Notes in Comput. Sci., vol. 7211, (2012), Springer), 194-213 · Zbl 1352.68182
[25] Ferrari, G. L.; Moggi, E.; Pugliese, R., Guardians for ambient-based monitoring, Electron. Notes Theor. Comput. Sci., 66, 3, 52-75, (2002)
[26] Gan, Y.; Chechik, M.; Nejati, S.; Bennett, J.; O’Farrell, B.; Waterhouse, J., Runtime monitoring of web service conversations, (CASCON, (2007), ACM), 42-57
[27] Ghezzi, C.; Guinea, S., Run-time monitoring in service-oriented architectures, (Test and Analysis of Web Services, (2007), Springer), 237-264
[28] Hamlen, K. W.; Jones, M., Aspect-oriented in-lined reference monitors, (PLAS, (2008), ACM), 11-20
[29] Havelund, K.; Goldberg, A., Verify your runs, (Verified Software: Theories, Tools, Experiments, (2008), Springer), 374-383
[30] Honda, K.; Hu, R.; Neykova, R.; Chen, T.-C.; Demangeon, R.; Deniélou, P.-M.; Yoshida, N., Structuring communication with session types, (COB, Lecture Notes in Comput. Sci., vol. 8665, (2012), Springer), 105-127
[31] Honda, K.; Mukhamedov, A.; Brown, G.; Chen, T.-C.; Yoshida, N., Scribbling interactions with a formal foundation, (ICDCIT, Lecture Notes in Comput. Sci., vol. 6536, (2011), Springer), 55-75
[32] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. Comput. Sci., 151, 2, 437-486, (1995) · Zbl 0871.68122
[33] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, (POPL, (2008), ACM), 273-284 · Zbl 1295.68150
[34] Hu, R.; Neykova, R.; Yoshida, N.; Demangeon, R., Practical interruptible conversations: distributed dynamic verification with session types and python, (RV, Lecture Notes in Comput. Sci., vol. 8174, (2013), Springer), 130-148
[35] Jia, L.; Gommerstadt, H.; Pfenning, F., Monitors and blame assignment for higher-order session types, (POPL, (2016), ACM), 582-594 · Zbl 1347.68269
[36] Krüger, I. H.; Meisinger, M.; Menarini, M., Runtime verification of interactions: from MSCs to aspects, (RV, Lecture Notes in Comput. Sci., vol. 4839, (2007), Springer), 63-74
[37] Krüger, I. H.; Meisinger, M.; Menarini, M., Interaction-based runtime verification for systems of systems integration, J. Logic Comput., 20, 3, 725-742, (2010)
[38] Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebr. Program., 78, 5, 293-303, (2009) · Zbl 1192.68433
[39] Ligatti, J.; Bauer, L.; Walker, D., Run-time enforcement of nonsafety policies, ACM Trans. Inf. Syst. Secur., 12, (2009)
[40] Mascardi, V.; Ancona, D., Attribute global types for dynamic checking of protocols in logic-based multiagent systems, Theory Pract. Log. Program., 13, 4-5 Online Supplement, (2013)
[41] Neykova, R.; Bocchi, L.; Yoshida, N., Timed runtime monitoring for multiparty conversations, (BEAT, Electron. Proc. Theor. Comput. Sci., vol. 162, (2014)), 19-26
[42] Neykova, R.; Yoshida, N., Multiparty session actors, (COORDINATION, Lecture Notes in Comput. Sci., vol. 8459, (2014), Springer), 131-146, a full version in LMCS
[43] Neykova, R.; Yoshida, N.; Hu, R., SPY: local verification of global protocols, (RV, Lecture Notes in Comput. Sci., vol. 8174, (2013), Springer), 358-363
[44] OOI
[45] Pierce, B. C., Types and programming languages, (2002), MIT Press
[46] Schneider, F. B., Enforceable security policies, ACM Trans. Inf. Syst. Secur., 3, 30-50, (2000)
[47] Scribble Project homepage
[48] Simmonds, J.; Gan, Y.; Chechik, M.; Nejati, S.; O’Farrell, B.; Litani, E.; Waterhouse, J., Runtime monitoring of web service conversations, IEEE Trans. Serv. Comput., 2, 3, 223-244, (2009)
[49] Sridhar, M.; Hamlen, K. W., Model-checking in-lined reference monitors, (VMCAI, Lecture Notes in Comput. Sci., vol. 5944, (2010), Springer), 312-327 · Zbl 1273.68241
[50] van der Aalst, W. M.P.; Dumas, M.; Ouyang, C.; Rozinat, A.; Verbeek, E., Conformance checking of service behavior, ACM Trans. Internet Techn., 8, 3, (2008)
[51] Yoshida, N.; Hu, R.; Neykova, R.; Ng, N., The scribble protocol language, (TGC, Lecture Notes in Comput. Sci., vol. 8358, (2013), Springer), 22-41
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.