Document Open Access Logo

Meeting Deadlines Together

Authors Laura Bocchi, Julien Lange, Nobuko Yoshida

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2015.283.pdf
  • Filesize: 0.7 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • timed automata
  • multiparty session types
  • global specification

Metrics

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

Abstract

This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory.

Cite As Get BibTex

Laura Bocchi, Julien Lange, and Nobuko Yoshida. Meeting Deadlines Together. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 283-296, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.283

Author Details

Laura Bocchi
Julien Lange
Nobuko Yoshida

References

  1. S. Akshay, Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Model checking time-constrained scenario-based specifications. In FSTTCS, volume 8 of LIPIcs, pages 204-215, 2010. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. TCS, 126:183-235, 1994. Google Scholar
  3. Webpage of this paper, 2015. URL: http://www.doc.ic.ac.uk/~jlange/cta/.
  4. Massimo Bartoletti, Tiziana Cimoli, Maurizio Murgia, Alessandro Sebastian Podda, and Livio Pompianu. Compliance and subtyping in timed session types. In FORTE, volume 9039 of LNCS, pages 161-177. Springer, 2015. Google Scholar
  5. Johan Bengtsson et al. Uppaal - a tool suite for automatic verification of real-time systems. In Hybrid Systems III, volume 1066 of LNCS, pages 232-243. Springer, 1996. Google Scholar
  6. Laura Bocchi, Weizhen Yang, and Nobuko Yoshida. Timed multiparty session types. In CONCUR, volume 8704 of LNCS, pages 419-434. Springer, 2014. Google Scholar
  7. Howard Bowman and Rodolfo Gómez. How to stop time stopping. FAC, 18(4):459-493, 2006. Google Scholar
  8. BPMN 2.0 Choreography, 2012. http://en.bpmn-community.org/tutorials/34/.
  9. Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. JACM, 30(2):323-342, 1983. Google Scholar
  10. Gérard Cécé and Alain Finkel. Verification of programs with half-duplex communication. I&C, 202(2):166-190, 2005. Google Scholar
  11. Prakash Chandrasekaran and Madhavan Mukund. Matching scenarios with timing constraints. In FORMATS, volume 4202 of LNCS, pages 98-112. Springer, 2006. Google Scholar
  12. Lorenzo Clemente, Frédéric Herbreteau, Amelie Stainer, and Grégoire Sutre. Reachability of communicating timed processes. In FOSSACS, volume 7794 of LNCS, pages 81-96. Springer, 2013. Google Scholar
  13. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In ESOP, volume 7211 of LNCS, pages 194-213. Springer, 2012. Google Scholar
  14. Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP (2), volume 7966 of LNCS, pages 174-186. Springer, 2013. Google Scholar
  15. Uno Holmer, Kim Guldstrand Larsen, and Wang Yi. Deciding properties of regular real time processes. In CAV, volume 575 of LNCS, pages 443-453. Springer, 1991. Google Scholar
  16. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, pages 273-284. ACM, 2008. Google Scholar
  17. Pavel Krcál and Wang Yi. Communicating timed automata: The more synchronous, the more difficult to verify. In CAV, volume 4144 of LNCS, pages 249-262, 2006. Google Scholar
  18. Julien Lange and Emilio Tuosto. Synthesising Choreographies from Local Session Types. In CONCUR, volume 7454 of LNCS, pages 225-239. Springer, 2012. Google Scholar
  19. Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL, pages 221-232, 2015. Google Scholar
  20. Rumyana Neykova, Laura Bocchi, and Nobuko Yoshida. Timed runtime monitoring for multiparty conversations. In BEAT, volume 162 of EPTCS, pages 19-26, 2014. Google Scholar
  21. Stavros Tripakis. Verifying progress in timed systems. In Formal Methods for Real-Time and Probabilistic Systems, volume 1601 of LNCS, pages 299-314. Springer, 1999. Google Scholar
  22. Stavros Tripakis, Sergio Yovine, and Ahmed Bouajjani. Checking timed büchi automata emptiness efficiently. Formal Methods in System Design, 26(3):267-292, 2005. Google Scholar
  23. Zero Deviation Lifecycle. URL: http://www.zdlc.co.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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