Document Open Access Logo

Progress-Preserving Refinements of CTA

Authors Massimo Bartoletti, Laura Bocchi, Maurizio Murgia

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.40.pdf
  • Filesize: 0.63 MB
  • 19 pages

Document Identifiers

Author Details

Massimo Bartoletti
  • Università degli Studi di Cagliari, Cagliari, Italy
Laura Bocchi
  • University of Kent, Canterbury, UK
Maurizio Murgia
  • University of Kent, Canterbury, UK

Funding

This work has been partially supported by EPSRC EP/N035372/1 "Time-sensitive protocol design and implementation", and by Aut. Reg. of Sardinia project P.I.A. 2013 "NOMAD".

Cite As Get BibTex

Massimo Bartoletti, Laura Bocchi, and Maurizio Murgia. Progress-Preserving Refinements of CTA. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.40

Abstract

We develop a theory of refinement for timed asynchronous systems, in the setting of Communicating Timed Automata (CTA). Our refinement applies point-wise to the components of a system of CTA, and only affecting their time constraints - in this way, we achieve compositionality and decidability. We then establish a decidable condition under which our refinement preserves behavioural properties of systems, such as their global and local progress. Our theory provides guidelines on how to implement timed protocols using the real-time primitives of programming languages. We validate our theory through a series of experiments, supported by an open-source tool which implements our verification techniques.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • protocol implementation
  • communicating timed automata
  • message passing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Shankara Narayanan Krishna. What is decidable about perfect timed channels? CoRR, abs/1708.05063, 2017. URL: http://arxiv.org/abs/1708.05063.
  2. Parosh Aziz Abdulla, Pavel Krcál, and Wang Yi. Sampled semantics of timed automata. Logical Methods in Computer Science, 6(3), 2010. URL: http://arxiv.org/abs/1007.2783.
  3. Luca Aceto, Matteo Cimini, Anna Ingólfsdóttir, Arni Hermann Reynisson, Steinar Hugi Sigurdarson, and Marjan Sirjani. Modelling and simulation of asynchronous real-time systems using timed Rebeca. Sci. Comput. Program., 89:41-68, 2014. Google Scholar
  4. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. Google Scholar
  5. Advanced Message Queuing protocols (AMQP) homepage. URL: https://www.amqp.org/.
  6. Joe Armstrong. Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf, 2007. Google Scholar
  7. Massimo Bartoletti, Tiziana Cimoli, and Maurizio Murgia. Timed session types. Logical Methods in Computer Science, 13(4), 2017. URL: http://dx.doi.org/10.23638/LMCS-13(4:25)2017.
  8. Massimo Bartoletti, Alceste Scalas, and Roberto Zunino. A semantic deconstruction of session types. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 402-418. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_28.
  9. Gerd Behrmann, Alexandre David, and Kim G. Larsen. A tutorial on Uppaal. In SFM, volume 3185 of Lecture Notes in Computer Science, pages 200-236. Springer, 2004. URL: http://dx.doi.org/10.1007/b110123.
  10. Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In Lectures on Concurrency and Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87-124. Springer, 2003. URL: http://dx.doi.org/10.1007/b98282.
  11. Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting deadlines together. In CONCUR, volume 42 of LIPIcs, pages 283-296. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.283.
  12. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. Timed multiparty session types. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 419-434. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_29.
  13. Sébastien Bornot, Joseph Sifakis, and Stavros Tripakis. Modeling urgency in timed systems. In COMPOS, volume 1536 of Lecture Notes in Computer Science, pages 103-129. Springer, 1997. URL: http://dx.doi.org/10.1007/3-540-49213-5_5.
  14. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323-342, 1983. Google Scholar
  15. Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300-320, 2017. Google Scholar
  16. Eric J. Bruno and Greg Bollella. Real-Time Java Programming: With Java RTS. Prentice Hall PTR, Upper Saddle River, NJ, USA, 1st edition, 2009. Google Scholar
  17. Stefano Cattani and Marta Z. Kwiatkowska. A refinement-based process algebra for timed automata. Formal Asp. Comput., 17(2):138-159, 2005. Google Scholar
  18. Karlis Cerans. Decidability of bisimulation equivalences for parallel timer processes. In CAV, volume 663 of Lecture Notes in Computer Science, pages 302-315. Springer, 1992. URL: http://dx.doi.org/10.1007/3-540-56496-9.
  19. Prakash Chandrasekaran and Madhavan Mukund. Matching scenarios with timing constraints. In FORMATS, volume 4202 of Lecture Notes in Computer Science, pages 98-112. Springer, 2006. URL: http://dx.doi.org/10.1007/11867340.
  20. Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types. Logical Methods in Computer Science, 13(2), 2017. Google Scholar
  21. Chris Chilton, Marta Z. Kwiatkowska, and Xu Wang. Revisiting timed specification theories: A linear-time perspective. In FORMATS, volume 7595 of Lecture Notes in Computer Science, pages 75-90. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33365-1_7.
  22. Lorenzo Clemente, Frédéric Herbreteau, Amélie Stainer, and Grégoire Sutre. Reachability of communicating timed processes. In FoSSaCS, volume 7794 of Lecture Notes in Computer Science, pages 81-96. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37075-5_6.
  23. Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, Louis-Marie Traonouez, and Andrzej Wasowski. Real-time specifications. STTT, 17(1):17-45, 2015. URL: http://dx.doi.org/10.1007/s10009-013-0286-x.
  24. Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR, volume 6901 of Lecture Notes in Computer Science, pages 280-296. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-23217-6_19.
  25. Henning Dierks, Sebastian Kupferschmid, and Kim Guldstrand Larsen. Automatic abstraction refinement for timed automata. In FORMATS, volume 4763 of Lecture Notes in Computer Science, pages 114-129. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-75454-1_10.
  26. Harald Fecher, Mila E. Majster-Cederbaum, and Jinzhao Wu. Refinement of actions in a real-time process algebra with a true concurrency model. Electr. Notes Theor. Comput. Sci., 70(3):260-280, 2002. URL: http://dx.doi.org/10.1016/S1571-0661(05)80496-7.
  27. Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time systems. Inf. Comput., 111(2):193-244, 1994. Google Scholar
  28. Jan Hoffmann and Zhong Shao. Automatic static cost analysis for parallel programs. In ESOP, volume 9032 of Lecture Notes in Computer Science, pages 132-157. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8.
  29. Pavel Krcál and Wang Yi. Communicating timed automata: The more synchronous, the more difficult to verify. In CAV, volume 4144 of Lecture Notes in Computer Science, pages 249-262. Springer, 2006. URL: http://dx.doi.org/10.1007/11817963.
  30. Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 441-457, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7.
  31. Kim G. Larsen, Axel Legay, Louis-Marie Traonouez, and Andrzej Wasowski. Robust synthesis for real-time systems. Theor. Comput. Sci., 515:96-122, 2014. URL: http://dx.doi.org/10.1016/j.tcs.2013.08.015.
  32. Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a nutshell. STTT, 1(1-2):134-152, 1997. Google Scholar
  33. Nancy A. Lynch, Roberto Segala, and Frits W. Vaandrager. Hybrid I/O automata. Inf. Comput., 185(1):105-157, 2003. Google Scholar
  34. Dimitris Mostrous. Session Types in Concurrent Calculi: Higher-Order Processes and Objects. PhD thesis, Imperial College London, November 2009. Google Scholar
  35. Dimitris Mostrous and Nobuko Yoshida. Session-based communication optimisation for higher-order mobile processes. In TLCA, volume 5608 of Lecture Notes in Computer Science, pages 203-218. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02273-9_16.
  36. Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP, volume 5502 of Lecture Notes in Computer Science, pages 316-332. Springer, 2009. Google Scholar
  37. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. Formal Asp. Comput., 29(5):877-910, 2017. URL: http://dx.doi.org/10.1007/s00165-017-0420-8.
  38. Xavier Nicollin and Joseph Sifakis. An overview and synthesis on timed process algebras. In CAV, volume 575 of Lecture Notes in Computer Science, pages 376-398. Springer, 1991. Google Scholar
  39. Julien Ponge, Boualem Benatallah, Fabio Casati, and Farouk Toumani. Analysis and applications of timed service protocols. ACM Trans. Softw. Eng. Methodol., 19(4):11:1-11:38, 2010. Google Scholar
  40. Steve Schneider. Concurrent and Real Time Systems: The CSP Approach. John Wiley &Sons, Inc., New York, NY, USA, 1st edition, 1999. Google Scholar
  41. The Simple Mail Transfer Protocol. URL: http://tools.ietf.org/html/rfc5321.
  42. Steve Vinoski. Advanced message queuing protocol. IEEE Internet Computing, 10(6):87-89, 2006. Google Scholar
  43. Weifeng Wang and Li Jiao. Trace abstraction refinement for timed automata. In ATVA, volume 8837 of Lecture Notes in Computer Science, pages 396-410. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11936-6.
  44. Sergio Yovine. Kronos: A verification tool for real-time systems. (Kronos user’s manual release 2.2). STTT, 1(1-2):123-133, 1997. URL: http://dx.doi.org/10.1007/s100090050009.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact