Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Etessami K, Yannakakis M (2005) Realizability and verification of {MSC} graphs. Theor Comput Sci 331(1): 97–114
Apt KR, Francez N, Katz S (1987) Appraising fairness in distributed languages. In: POPL, pp 189–198. ACM
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
Abdallah R, Hélouët L, Jard C (2015) Distributed implementation of message sequence charts. Softw Syst Model 14(2): 1029–1048
Advanced Message Queuing protocols (AMQP) homepage. http://jira.amqp.org/confluence/display/AMQP/Advanced+Message+Queuing+Protocol.
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
Bocchi L, Demangeon R, Yoshida N (2012) A multiparty multi-session logic. In: TGC, vol 8191 of LNCS, Springer, Berlin, pp 97–111
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
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
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
Berger M, Yoshida N (2007) Timed, distributed, probabilistic, typed processes. In: APLAS, vol 4807 of LNCS, pp 158–174
Bocchi L, Yang W, Yoshida N (2014) Timed multiparty session types. In: CONCUR, vol 8704 of LNCS, Springer, Berlin, pp 419–434
Bocchi L, Yang W, Yoshida N (2014) Timed multiparty session types. Technical Report 2014/3, Department of Computing, Imperial College London
Cambronero M-E et al (2011) Validation and verification of web services choreographies by using timed automata. J Log Algebr Program 80(1): 25–49
Coppo M, Dezani-Ciancaglini M, Yoshida N, Padovani L (2015) Global progress for dynamically interleaved multiparty sessions. MSCS 760: 1–65
Cheikhrouhou S, Kallel S, Guermouche N, Jmaiel M (2013) A survey on time-aware business process modeling. In: ICEIS (3), pp 236–242. SciTePress
Colombo C, Pace GJ, Schneider G (2009) Larva—safer monitoring of real-time java programs (tool paper). In: SEFM, pp 33–37
Chen F, Rosu G (2007) Mop: an efficient and generic runtime verification framework. In: OOPSLA, pp 569–588
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
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
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
Georges A, Buytaert D, Eeckhout L (2007) Statistically rigorous java performance evaluation. SIGPLAN Not 42(10): 57–76
Guermouche N, Dal-Zilio S (2012) Towards timed requirement verification for service choreographies. In: CollaborateCom, pp 117–126. IEEE
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
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
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
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
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
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
Hu R, Yoshida N (2016) Hybrid session verification through endpoint api generation. In: FASE 2016, LNCS. Springer, Berlin
Honda K, Yoshida N, Carbone M (2008) Multiparty asynchronous session types. In: POPL, pp 273–284. ACM
International Telecommunication Union. Recommendation Z.120: Message sequence chart (1998)
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
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
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
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
Lohrey M (2003) Realizability of high-level message sequence charts: closing the gaps. Theor Comput Sci 309(1): 529–554
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
Lapadula A, Pugliese R, Tiezzi F (2007) Cows: a timed service-oriented calculus. In: ICTAC, vol 4711 of LNCS, pp 275–290
Lee JY, Zic J (2002) On modeling real-time mobile processes. Aust Comput Sci Commun 24(1): 139–147
Laneve C, Zavattaro G (2005) Foundations of web transactions. In: FOSSACS, vol 3411 of LNCS, pp 282–298
Minsky NH, Ungureanu V (2000) Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems. TOSEM 9: 273–305
Neykova R, Yoshida N, Hu R (2013) SPY: local verification of global protocols. In: RV, vol 8174, Springer, Berlin, pp 358–363
Ocean Observatories Initiative (OOI) http://oceanobservatories.org/
Timed Conversation API in Python. http://www.doc.ic.ac.uk/~rn710/TimeApp.html
Scribble Project homepage. http://www.scribble.org
Saeedloei N, Gupta G (2013) Timed π-calculus. In: TGC, vol 8358 of LNCS. Springer, Berlin, pp 119–135
Skiena SS (2008) The algorithm design manual, 2nd edn. Springer, Berlin
The Simple Mail Transfer Protocol. http://tools.ietf.org/html/rfc5321
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
UPPAAL tool website. http://www.uppaal.org/
Kenji W, Ishikawa F, Hiraishi K (2011) Formal verification of business processes with temporal and resource constraints. In: SMC, pp 1173–1180. IEEE
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
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
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
Z3 smt solver. http://z3.codeplex.com/
Author information
Authors and Affiliations
Corresponding author
Additional information
Thomas Hildebrandt, Joachim Parrow and Marco Carbone
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Neykova, R., Bocchi, L. & Yoshida, N. Timed runtime monitoring for multiparty conversations. Form Asp Comp 29, 877–910 (2017). https://doi.org/10.1007/s00165-017-0420-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-017-0420-8