Document Open Access Logo

Local Planning Semantics: A Semantics for Distributed Real-Time Systems

Authors Mahieddine Dellabani , Jacques Combaz , Saddek Bensalem , Marius Bozga

PDF
Thumbnail PDF

File

LITES-v006-i001-a001.pdf
  • Filesize: 0.87 MB
  • 27 pages

Document Identifiers

Author Details

Mahieddine Dellabani
  • University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, 38000 Grenoble, France
Jacques Combaz
  • University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, 38000 Grenoble, France
Saddek Bensalem
  • University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, 38000 Grenoble, France
Marius Bozga
  • University Grenoble Alpes, CNRS, Grenoble INP (Institute of Engineering Univ. Grenoble Alpes), VERIMAG, 38000 Grenoble, France

Cite AsGet BibTex

Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga. Local Planning Semantics: A Semantics for Distributed Real-Time Systems. In LITES, Volume 6, Issue 1 (2019). Leibniz Transactions on Embedded Systems, Volume 6, Issue 1, pp. 01:1-01:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LITES-v006-i001-a001

Abstract

Design, implementation and verification of distributed real-time systems are acknowledged to be very hard tasks. Such systems are prone to different kinds of delay, such as execution time of actions or communication delays implied by distributed platforms. The latter increase considerably the complexity of coordinating the parallel activities of running components. Scheduling such systems must cope with those delays by proposing execution strategies  ensuring global consistency while satisfying the imposed timing constraints. In this paper, we investigate a formal model for such systems as compositions of timed automata subject to multiparty interactions, and propose a semantics aiming to overcome the communication delays problem through anticipating the execution of interactions. To be effective in a distributed context, scheduling an interaction should rely on (as much as possible) local information only, namely the state of its participating components. However, as shown in this paper these information is not always sufficient and does not guarantee a safe execution of the system as it may introduce deadlocks. Moreover, delays may also affect the satisfaction of timing constraints, which also corresponds to deadlocks in the former model. Thus, we also explore methods for analyzing such deadlock situations and for computing  deadlock-free scheduling strategies when possible.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Distributed Real-Time Systems
  • Timed Automata
  • Formal Verification

Metrics

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

References

  1. Tesnim Abdellatif, Jacques Combaz, and Joseph Sifakis.Model-based implementation of real-time applications. In Proceedings of the 10th International conference on Embedded software, EMSOFT 2010, Scottsdale, Arizona, USA, October 24-29, 2010, pages 229-238, 2010. URL: http://dx.doi.org/10.1145/1879021.1879052
  2. Karine Altisen, Gregor Gößler, and Joseph Sifakis.Scheduler Modeling Based on the Controller Synthesis Paradigm. Real-Time Systems, 23(1-2):55-84, 2002. URL: http://dx.doi.org/10.1023/A:1015346419267
  3. Karine Altisen and Stavros Tripakis.Implementation of Timed Automata: An Issue of Semantics or Modeling? In Formal Modeling and Analysis of Timed Systems, Third International Conference, FORMATS 2005, Uppsala, Sweden, September 26-28, 2005, Proceedings, pages 273-288, 2005. URL: http://dx.doi.org/10.1007/11603009_21
  4. Rajeev Alur and David L. Dill.A Theory of Timed Automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90010-8
  5. Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, and Joseph Sifakis.Using BIP for Modeling and Verification of Networked Systems - A Case Study on TinyOS-based Networks. In Sixth IEEE International Symposium on Network Computing and Applications (NCA 2007), 12 - 14 July 2007, Cambridge, MA, USA, pages 257-260, 2007. URL: http://dx.doi.org/10.1109/NCA.2007.52
  6. Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime.UPPAAL-Tiga: Time for Playing Games! In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pages 121-125, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73368-3_14
  7. Johan Bengtsson and Wang Yi.On Clock Difference Constraints and Termination in Reachability Analysis of Timed Automata. In Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings, pages 491-503, 2003. URL: http://dx.doi.org/10.1007/978-3-540-39893-6_28
  8. Saddek Bensalem, Marius Bozga, Jean Quilbeuf, and Joseph Sifakis.Optimized distributed implementation of multiparty interactions with observation. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions, AGERE! 2012, October 21-22, 2012, Tucson, Arizona, USA, pages 71-82, 2012. URL: http://dx.doi.org/10.1145/2414639.2414649
  9. Gérard Berry and Georges Gonthier.The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Sci. Comput. Program., 19(2):87-152, 1992. URL: http://dx.doi.org/10.1016/0167-6423(92)90005-V
  10. Borzoo Bonakdarpour, Marius Bozga, and Jean Quilbeuf.Model-based implementation of distributed systems with priorities. Design Autom. for Emb. Sys., 17(2):251-276, 2013. URL: http://dx.doi.org/10.1007/s10617-012-9091-0
  11. Sylvain Camier, Damien Chabrol, Vincent David, and Christophe Aussaguès.OASIS formal approach for distributed safety-critical real-time system design. In ISoLA 2007, Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Poitiers-Futuroscope, France, December 12-14, 2007, pages 167-178, 2007. URL: http://editions-rnti.fr/?inprocid=1000543.
  12. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime.Efficient On-the-Fly Algorithms for the Analysis of Timed Games. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, pages 66-80, 2005. URL: http://dx.doi.org/10.1007/11539452_9
  13. Robert N. Charette.This Car Runs on Code. IEEE Spectrum, 2009. Google Scholar
  14. Conrado Daws, Marta Z. Kwiatkowska, and Gethin Norman.Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM.STTT, 5(2-3):221-236, 2004. URL: http://dx.doi.org/10.1007/s10009-003-0118-5
  15. Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga.Knowledge Based Optimization for Distributed Real-Time Systems. In 24th Asia-Pacific Software Engineering Conference, APSEC 2017, Nanjing, China, December 4-8, 2017, pages 751-756, 2017. URL: http://dx.doi.org/10.1109/APSEC.2017.106
  16. Mahieddine Dellabani, Jacques Combaz, Marius Bozga, and Saddek Bensalem.Local Planning of Multiparty Interactions with Bounded Horizons. In FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, pages 199-216, 2016. URL: http://dx.doi.org/10.1007/978-3-319-48989-6_13
  17. Bruno Dutertre and Leonardo de Moura.The Yices SMT solver. Technical report, SRI International, 2006. Google Scholar
  18. Nicolas Halbwachs, Fabienne Lagnier, and Christophe Ratel.Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE.IEEE Trans. Software Eng., 18(9):785-793, 1992. URL: http://dx.doi.org/10.1109/32.159839
  19. Thomas A. Henzinger, Benjamin Horowitz, and Christoph M. Kirsch.Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE, 91(1):84-99, 2003. Google Scholar
  20. Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.Symbolic Model Checking for Real-Time Systems. Inf. Comput., 111(2):193-244, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1045
  21. BaekGyu Kim, Lu Feng, Linh T. X. Phan, Oleg Sokolsky, and Insup Lee.Platform-specific timing verification framework in model-based implementation. In Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, Grenoble, France, March 9-13, 2015, pages 235-240, 2015. URL: http://dl.acm.org/citation.cfm?id=2755804.
  22. BaekGyu Kim, Lu Feng, Oleg Sokolsky, and Insup Lee.Platform-Specific Code Generation from Platform-Independent Timed Models. In 2015 IEEE Real-Time Systems Symposium, RTSS 2015, San Antonio, Texas, USA, December 1-4, 2015, pages 75-86, 2015. URL: http://dx.doi.org/10.1109/RTSS.2015.15
  23. Christos Kloukinas and Sergio Yovine.A model-based approach for multiple QoS in scheduling: from models to implementation. Autom. Softw. Eng., 18(1):5-38, 2011. URL: http://dx.doi.org/10.1007/s10515-010-0074-8
  24. Hermann Kopetz.An Integrated Architecture for Dependable Embedded Systems. In 23rd International Symposium on Reliable Distributed Systems (SRDS 2004), 18-20 October 2004, Florianpolis, Brazil, pages 160-161, 2004. URL: http://dx.doi.org/10.1109/RELDIS.2004.1353016
  25. Magnus Lindahl, Paul Pettersson, and Wang Yi.Formal Design and Analysis of a Gear Controller. In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, pages 281-297, 1998. URL: http://dx.doi.org/10.1007/BFb0054178
  26. Braham Lotfi Mediouni, Ayoub Nouri, Marius Bozga, Mahieddine Dellabani, Jacques Combaz, Axel Legay, and Saddek Bensalem.SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems. Technical Report TR-2018-5, Verimag Research Report, 2018. Google Scholar
  27. Souha Ben Rayana, Marius Bozga, Saddek Bensalem, and Jacques Combaz.RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, pages 394-406, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49674-9_23
  28. Ahlem Triki.Distributed Implementations of Timed Component-based Systems. (Implémentations distribuées des systèmes temps-réel à base de composants). PhD thesis, Grenoble Alpes University, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01169720.
  29. Ahlem Triki, Borzoo Bonakdarpour, Jacques Combaz, and Saddek Bensalem.Automated Conflict-Free Concurrent Implementation of Timed Component-Based Models. In NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings, pages 359-374, 2015. URL: http://dx.doi.org/10.1007/978-3-319-17524-9_25
  30. Stavros Tripakis.L'analyse formelle des systèmes temporisés en pratique. (The Formal Analysis of Timed Systems in Practice). PhD thesis, Joseph Fourier University, Grenoble, France, 1998. URL: https://tel.archives-ouvertes.fr/tel-00004907.
  31. Stavros Tripakis.Verifying Progress in Timed Systems. In Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999. Proceedings, pages 299-314, 1999. URL: http://dx.doi.org/10.1007/3-540-48778-6_18
  32. Martin De Wulf, Laurent Doyen, and Jean-François Raskin.Almost ASAP Semantics: From Timed Models to Timed Implementations. In Hybrid Systems: Computation and Control, 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25-27, 2004, Proceedings, pages 296-310, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24743-2_20
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 Imprint Privacy Contact