Local Planning Semantics: A Semantics for Distributed Real-Time Systems
- Distributed Real-Time Systems,
- Timed Automata,
- Formal Verification
Copyright (c) 2019 Mahieddine Dellabani, Jacques Combaz, Saddek Bensalem, and Marius Bozga
This work is licensed under a Creative Commons Attribution 3.0 Unported License.
How to Cite
AbstractDesign, 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.
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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.
- 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
- Robert N. Charette.This Car Runs on Code. IEEE Spectrum, 2009.
- 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
- 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
- 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
- Bruno Dutertre and Leonardo de Moura.The Yices SMT solver. Technical report, SRI International, 2006.
- 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
- 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.
- 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
- 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.
- 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
- 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
- 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
- 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
- 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.
- 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
- 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.
- 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
- 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.
- 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
- 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