{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:00Z","timestamp":1780994700638,"version":"3.54.1"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K034413\/1"],"award-info":[{"award-number":["EP\/K034413\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K011715\/1"],"award-info":[{"award-number":["EP\/K011715\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L00058X\/1"],"award-info":[{"award-number":["EP\/L00058X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N027833\/1"],"award-info":[{"award-number":["EP\/N027833\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N028201\/1"],"award-info":[{"award-number":["EP\/N028201\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Seventh Framework Programme (BE)","award":["612985 (UPSCALE)."],"award-info":[{"award-number":["612985 (UPSCALE)."]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-017-0420-8","type":"journal-article","created":{"date-parts":[[2017,2,22]],"date-time":"2017-02-22T08:04:41Z","timestamp":1487750681000},"page":"877-910","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":34,"title":["Timed runtime monitoring for multiparty conversations"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2755-7728","authenticated-orcid":false,"given":"Rumyana","family":"Neykova","sequence":"first","affiliation":[{"name":"Imperial College London, 180 Queens Gate, SW7 2AZ, Kensington, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Laura","family":"Bocchi","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, 180 Queens Gate, SW7 2AZ, Kensington, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.034"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Apt KR Francez N Katz S (1987) Appraising fairness in distributed languages. In: POPL pp 189\u2013198. ACM","DOI":"10.1145\/41625.41642"},{"key":"e_1_2_1_2_3_2","unstructured":"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\u2013215"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0357-1"},{"key":"e_1_2_1_2_5_2","unstructured":"Advanced Message Queuing protocols (AMQP) homepage. http:\/\/jira.amqp.org\/confluence\/display\/AMQP\/Advanced+Message+Queuing+Protocol."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"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\u201365","DOI":"10.1007\/978-3-642-38592-6_5"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bocchi L Demangeon R Yoshida N (2012) A multiparty multi-session logic. In: TGC vol 8191 of LNCS Springer Berlin pp 97\u2013111","DOI":"10.1007\/978-3-642-41157-1_7"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bowman H Faconti GP Massink M (1998) Specification and verification of media constraints using UPAAL. In: Design specification and verification of interactive systems\u201998 proceedings of the fifth international eurographics workshop 1998 Abingdon Springer UK pp 261\u2013277","DOI":"10.1007\/978-3-7091-3693-5_17"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"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\u2013176","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_2_1_2_10_2","unstructured":"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\u2013296. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Berger M Yoshida N (2007) Timed distributed probabilistic typed processes. In: APLAS vol 4807 of LNCS pp 158\u2013174","DOI":"10.1007\/978-3-540-76637-7_11"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bocchi L Yang W Yoshida N (2014) Timed multiparty session types. In: CONCUR vol 8704 of LNCS Springer Berlin pp 419\u2013434","DOI":"10.1007\/978-3-662-44584-6_29"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bocchi L Yang W Yoshida N (2014) Timed multiparty session types. Technical Report 2014\/3 Department of Computing Imperial College London","DOI":"10.1007\/978-3-662-44584-6_29"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.02.001"},{"key":"e_1_2_1_2_15_2","first-page":"1","article-title":"Global progress for dynamically interleaved multiparty sessions","volume":"760","author":"Coppo M","year":"2015","journal-title":"MSCS"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Cheikhrouhou S Kallel S Guermouche N Jmaiel M (2013) A survey on time-aware business process modeling. In: ICEIS (3) pp 236\u2013242. SciTePress","DOI":"10.5220\/0004413202360242"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Colombo C Pace GJ Schneider G (2009) Larva\u2014safer monitoring of real-time java programs (tool paper). In: SEFM pp 33\u201337","DOI":"10.1109\/SEFM.2009.13"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Chen F Rosu G (2007) Mop: an efficient and generic runtime verification framework. In: OOPSLA pp 569\u2013588","DOI":"10.1145\/1297105.1297069"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"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\u201326","DOI":"10.1007\/978-3-642-55099-7_1"},{"key":"e_1_2_1_2_20_2","unstructured":"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\u201329"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou P-M Yoshida N (2013) Multiparty compatibility in communicating automata: characterisation and synthesis of global session types. In: Automata languages and programming\u201440th international colloquium ICALP 2013 Riga Latvia July 8\u201312 2013 Proceedings Part II volume 7966 of Lecture Notes in Computer Science Springer Berlin pp 174\u2013186","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297033"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Guermouche N Dal-Zilio S (2012) Towards timed requirement verification for service choreographies. In: CollaborateCom pp 117\u2013126. IEEE","DOI":"10.4108\/icst.collaboratecom.2012.250441"},{"key":"e_1_2_1_2_24_2","unstructured":"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\u2013183. Universities Press"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Gregorio-Rodrguez C et\u00a0al (1997) Testing semantics for a probabilistic-timed process algebra. In: Transformation-based reactive systems development vol 1231 of LNCS pp 353\u2013367","DOI":"10.1007\/3-540-63010-4_24"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"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\u2013127","DOI":"10.1007\/978-3-662-44471-9_5"},{"key":"e_1_2_1_2_27_2","unstructured":"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"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-642-19056-8_4"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"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\u2013148","DOI":"10.1007\/978-3-642-40787-1_8"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Hu R Yoshida N (2016) Hybrid session verification through endpoint api generation. In: FASE 2016 LNCS. Springer Berlin","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Honda K Yoshida N Carbone M (2008) Multiparty asynchronous session types. In: POPL pp 273\u2013284. ACM","DOI":"10.1145\/1328897.1328472"},{"key":"e_1_2_1_2_32_2","unstructured":"International Telecommunication Union. Recommendation Z.120: Message sequence chart (1998)"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"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\u201311 Nov 2009 Eindhoven The Netherlands pp 148\u2013157","DOI":"10.1109\/ECOWS.2009.15"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"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\u2013262","DOI":"10.1007\/11817963_24"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Krcal P Yi W (2006) Communicating timed automata: the more synchronous the more difficult to verify. In: CAV vol 4144 of LNCS pp 243\u2013257","DOI":"10.1007\/11817963_24"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"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 \u201906. New York pp 5\u201312. ACM","DOI":"10.1145\/1138953.1138956"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.08.002"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"L\u00f3pez HA P\u00e9rez JA (2012) Time and exceptional behavior in multiparty structured interactions. In: WS-FM vol 7176 of LNCS pp 48\u201363","DOI":"10.1007\/978-3-642-29834-9_5"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Lapadula A Pugliese R Tiezzi F (2007) Cows: a timed service-oriented calculus. In: ICTAC vol 4711 of LNCS pp 275\u2013290","DOI":"10.1007\/978-3-540-75292-9_19"},{"issue":"1","key":"e_1_2_1_2_40_2","first-page":"139","article-title":"On modeling real-time mobile processes","volume":"24","author":"Lee JY","year":"2002","journal-title":"Aust Comput Sci Commun"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Laneve C Zavattaro G (2005) Foundations of web transactions. In: FOSSACS vol 3411 of LNCS pp 282\u2013298","DOI":"10.1007\/978-3-540-31982-5_18"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/352591.352592"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Neykova R Yoshida N Hu R (2013) SPY: local verification of global protocols. In: RV vol 8174 Springer Berlin pp 358\u2013363","DOI":"10.1007\/978-3-642-40787-1_25"},{"key":"e_1_2_1_2_44_2","unstructured":"Ocean Observatories Initiative (OOI) http:\/\/oceanobservatories.org\/"},{"key":"e_1_2_1_2_45_2","unstructured":"Timed Conversation API in Python. http:\/\/www.doc.ic.ac.uk\/~rn710\/TimeApp.html"},{"key":"e_1_2_1_2_46_2","unstructured":"Scribble Project homepage. http:\/\/www.scribble.org"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Saeedloei N Gupta G (2013) Timed \u03c0-calculus. In: TGC vol 8358 of LNCS. Springer Berlin pp 119\u2013135","DOI":"10.1007\/978-3-319-05119-2_8"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/1410219"},{"key":"e_1_2_1_2_49_2","unstructured":"The Simple Mail Transfer Protocol. http:\/\/tools.ietf.org\/html\/rfc5321"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"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\u2013314","DOI":"10.1007\/3-540-48778-6_18"},{"key":"e_1_2_1_2_51_2","unstructured":"UPPAAL tool website. http:\/\/www.uppaal.org\/"},{"key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","unstructured":"Kenji W Ishikawa F Hiraishi K (2011) Formal verification of business processes with temporal and resource constraints. In: SMC pp 1173\u20131180. IEEE","DOI":"10.1109\/ICSMC.2011.6083857"},{"key":"e_1_2_1_2_53_2","doi-asserted-by":"crossref","unstructured":"Yoshida N Deni\u00e9lou P-M Bejleri A Hu R (2010) Parameterised multiparty session types. In: FoSSaCs\u201910 vol 6014 of LNCS Springer Berlin pp 128\u2013145","DOI":"10.1007\/978-3-642-12032-9_10"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Ye W Heidemann J Estrin D (2002) An energy-efficient mac protocol for wireless sensor networks. In: INFOCOM 2002 vol 3 pp 1567\u20131576. IEEE","DOI":"10.1109\/INFCOM.2002.1019408"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Yoshida N Hu R Neykova R Ng N (2013) The scribble protocol language. In: TGC 2013 vol 8358 of LNCS Springer Berlin pp 22\u201341","DOI":"10.1007\/978-3-319-14128-2_3"},{"key":"e_1_2_1_2_56_2","unstructured":"Z3 smt solver. http:\/\/z3.codeplex.com\/"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0420-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0420-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0420-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0420-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T15:34:00Z","timestamp":1750001640000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0420-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":56,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-017-0420-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0420-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}