zbMATH — the first resource for mathematics

Timed runtime monitoring for multiparty conversations. (English) Zbl 1375.68030
Summary: We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, which we have developed with our industrial partners. Drawing from recent work on multiparty session types for real-time interactions, we extend Scribble with clocks, resets, and clock predicates in order to constrain the times in which interactions occur. We present a timed API for Python to program distributed implementations of Scribble specifications. A dynamic verification framework ensures the safe execution of applications written with our timed API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing with respect to the corresponding Scribble specification. To demonstrate the practicality of the proposed framework, we express and verify four categories of widely used temporal patterns from use cases in literature. We analyse the performance of our implementation via benchmarking and show negligible overhead.

68M14 Distributed systems
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Alur, R; Etessami, K; Yannakakis, M, Realizability and verification of {MSC} graphs, Theor Comput Sci, 331, 97-114, (2005) · Zbl 1088.68097
[2] Apt KR, Francez N, Katz S (1987) Appraising fairness in distributed languages. In: POPL, pp 189-198. ACM · Zbl 0659.68023
[3] Akshay S, Gastin P, Mukund M, Narayan Kumar K (2010) Model checking time-constrained scenario-based specifications. In: FSTTCS, vol 8 of LIPIcs, pp 204-215 · Zbl 1245.68129
[4] Abdallah, R; Hélouët, L; Jard, C, Distributed implementation of message sequence charts, Softw Syst Model, 14, 1029-1048, (2015)
[5] Advanced Message Queuing protocols (AMQP) homepage. http://jira.amqp.org/confluence/display/AMQP/Advanced+Message+Queuing+Protocol. · Zbl 1207.68082
[6] Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida N (2013) Monitoring networks through multiparty session types. In: FORTE, vol 7892 of LNCS, pp 50-65 · Zbl 1359.68215
[7] Bocchi L, Demangeon R, Yoshida N (2012) A multiparty multi-session logic. In: TGC, vol 8191 of LNCS, Springer, Berlin, pp 97-111 · Zbl 1207.68082
[8] Bowman H, Faconti GP, Massink M (1998) Specification and verification of media constraints using UPAAL. In: Design, specification and verification of interactive systems’98, proceedings of the fifth international eurographics workshop, 1998, Abingdon, Springer, UK, pp 261-277 · Zbl 1070.68091
[9] Bocchi L, Honda K, Tuosto E, Yoshida N (2010) A theory of design-by-contract for distributed multiparty interactions. In: CONCUR, vol 6269 of LNCS, pp 162-176 · Zbl 1287.68121
[10] Bocchi L, Lange J, Yoshida N (2015) Meeting deadlines together. In: 26th International conference on concurrency theory, CONCUR 2015, Madrid, Spain, Sept 1.4, 2015, vol 42 of LIPIcs, pp 283-296. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik · Zbl 1374.68320
[11] Berger M, Yoshida N (2007) Timed, distributed, probabilistic, typed processes. In: APLAS, vol 4807 of LNCS, pp 158-174 · Zbl 1137.68442
[12] Bocchi L, Yang W, Yoshida N (2014) Timed multiparty session types. In: CONCUR, vol 8704 of LNCS, Springer, Berlin, pp 419-434 · Zbl 1417.68117
[13] Bocchi L, Yang W, Yoshida N (2014) Timed multiparty session types. Technical Report 2014/3, Department of Computing, Imperial College London · Zbl 1417.68117
[14] Cambronero, M-E; etal., Validation and verification of web services choreographies by using timed automata, J Log Algebr Program, 80, 25-49, (2011) · Zbl 1207.68082
[15] Coppo, M; Dezani-Ciancaglini, M; Yoshida, N; Padovani, L, Global progress for dynamically interleaved multiparty sessions, MSCS, 760, 1-65, (2015) · Zbl 1361.68165
[16] Cheikhrouhou S, Kallel S, Guermouche N, Jmaiel M (2013) A survey on time-aware business process modeling. In: ICEIS (3), pp 236-242. SciTePress · Zbl 1088.68097
[17] Colombo C, Pace GJ, Schneider G (2009) Larva—safer monitoring of real-time java programs (tool paper). In: SEFM, pp 33-37
[18] Chen F, Rosu G (2007) Mop: an efficient and generic runtime verification framework. In: OOPSLA, pp 569-588
[19] de Boer FS, de Gouw S, Johnsen EB, Kohn A, Wong PYH (2014) Run-time assertion checking of data- and protocol-oriented properties of Java programs: an industrial case study. Trans Aspect-Oriented Softw Dev 11:1-26 · Zbl 1070.68091
[20] Demangeon R, Honda K, Hu R, Neykova R, Yoshida N (2015) Practical interruptible conversations: Distributed dynamic verication with multiparty session types and python. FMSD, pp 1-29 · Zbl 1341.68118
[21] Deniélou P-M, Yoshida N (2013) Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Automata, languages, and programming—40th international colloquium, ICALP 2013, Riga, Latvia, July 8-12, 2013, Proceedings, Part II, volume 7966 of Lecture Notes in Computer Science, Springer, Berlin, pp 174-186 · Zbl 1334.68149
[22] Georges, A; Buytaert, D; Eeckhout, L, Statistically rigorous Java performance evaluation, SIGPLAN Not, 42, 57-76, (2007)
[23] Guermouche N, Dal-Zilio S (2012) Towards timed requirement verification for service choreographies. In: CollaborateCom, pp 117-126. IEEE
[24] Gastin P, Mukund M, Kumar KN (2009) Reachability and boundedness in time-constrained MSC graphs. In: Lodaya K, Mukund M, Ramanujam R (eds) Perspectives in concurrency theory, pp 157-183. Universities Press · Zbl 1193.68048
[25] Gregorio-Rodrguez C et al (1997) Testing semantics for a probabilistic-timed process algebra. In: Transformation-based reactive systems development, vol 1231 of LNCS, pp 353-367 · Zbl 1070.68091
[26] Honda K, Hu R, Neykova R, Chen T-C, Demangeon R, Denilou P-M, Yoshida N (2014) Structuring communication with session types. In: COB 2014, vol 8665 of LNCS, Springer, Berlin, pp 105-127
[27] Hlout L, Jard C (2000) Conditions for synthesis of communicating automata from hmscs. In: 5th International workshop on formal methods for industrial Cr itical systems (FMICS), Berlin, GMD FOKUS
[28] Honda K, Mukhamedov A, Brown G, Chen T-C, Yoshida N (2011) Scribbling interactions with a formal foundation. In: ICDCIT 2011, vol 6536 of LNCS. Springer, Berlin
[29] Hu R, Neykova R, Yoshida N, Demangeon R, Honda K (2013) Practical interruptible conversations: distributed dynamic verification with session types and python. In: RV, vol 8174 of LNCS, pp 130-148 · Zbl 1341.68118
[30] Hu R, Yoshida N (2016) Hybrid session verification through endpoint api generation. In: FASE 2016, LNCS. Springer, Berlin
[31] Honda K, Yoshida N, Carbone M (2008) Multiparty asynchronous session types. In: POPL, pp 273-284. ACM · Zbl 1295.68150
[32] International Telecommunication Union. Recommendation Z.120: Message sequence chart (1998)
[33] Kallel S, Charfi A, Dinkelaker T, Mezini M, Jmaiel M (2009) Specifying and monitoring temporal properties in web services compositions. In: Seventh IEEE European Conference on Web Services (ECOWS 2009), 9-11 Nov 2009, Eindhoven, The Netherlands, pp 148-157
[34] Krcal P, Yi W (2006) Communicating timed automata: the more synchronous, the more difficult to verify. In: Computer aided verification, vol 4144 of LNCS, Springer, Berlin, pp 249-262 · Zbl 1188.68192
[35] Krcal P, Yi W (2006) Communicating timed automata: the more synchronous, the more difficult to verify. In: CAV, vol 4144 of LNCS, pp 243-257 · Zbl 1188.68192
[36] Liang H, Dingel J, Diskin Z (2006) A comparative survey of scenario-based to state-based model synthesis approaches. In: International workshop on scenarios and state machines: models, algorithms, and tools, SCESM ’06. New York, pp 5-12. ACM
[37] Lohrey, M, Realizability of high-level message sequence charts: closing the gaps, Theor Comput Sci, 309, 529-554, (2003) · Zbl 1070.68091
[38] López HA, Pérez JA (2012) Time and exceptional behavior in multiparty structured interactions. In: WS-FM, vol 7176 of LNCS, pp 48-63
[39] Lapadula A, Pugliese R, Tiezzi F (2007) Cows: a timed service-oriented calculus. In: ICTAC, vol 4711 of LNCS, pp 275-290 · Zbl 1147.68846
[40] Lee, JY; Zic, J, On modeling real-time mobile processes, Aust Comput Sci Commun, 24, 139-147, (2002)
[41] Laneve C, Zavattaro G (2005) Foundations of web transactions. In: FOSSACS, vol 3411 of LNCS, pp 282-298 · Zbl 1118.68335
[42] Minsky, NH; Ungureanu, V, Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems, TOSEM, 9, 273-305, (2000)
[43] Neykova R, Yoshida N, Hu R (2013) SPY: local verification of global protocols. In: RV, vol 8174, Springer, Berlin, pp 358-363
[44] Ocean Observatories Initiative (OOI) http://oceanobservatories.org/
[45] Timed Conversation API in Python. http://www.doc.ic.ac.uk/ rn710/TimeApp.html
[46] Scribble Project homepage. http://www.scribble.org
[47] Saeedloei N, Gupta G (2013) Timed π-calculus. In: TGC, vol 8358 of LNCS. Springer, Berlin, pp 119-135 · Zbl 1348.68169
[48] Skiena SS (2008) The algorithm design manual, 2nd edn. Springer, Berlin · Zbl 1149.68081
[49] The Simple Mail Transfer Protocol. http://tools.ietf.org/html/rfc5321
[50] Tripakis S (1999) Verifying progress in timed systems. In: Formal methods for real-time and probabilistic systems, vol 1601 of LNCS, Springer, Berlin, pp 299-314
[51] UPPAAL tool website. http://www.uppaal.org/ · Zbl 1088.68097
[52] Kenji W, Ishikawa F, Hiraishi K (2011) Formal verification of business processes with temporal and resource constraints. In: SMC, pp 1173-1180. IEEE
[53] Yoshida N, Deniélou P-M, Bejleri A, Hu R (2010) Parameterised multiparty session types. In: FoSSaCs’10, vol 6014 of LNCS, Springer, Berlin, pp 128-145 · Zbl 1284.68077
[54] Ye W, Heidemann J, Estrin D (2002) An energy-efficient mac protocol for wireless sensor networks. In: INFOCOM 2002, vol 3, pp 1567-1576. IEEE
[55] Yoshida N, Hu R, Neykova R, Ng N (2013) The scribble protocol language. In: TGC 2013, vol 8358 of LNCS, Springer, Berlin, pp 22-41
[56] Z3 smt solver. http://z3.codeplex.com/
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.