{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T01:57:09Z","timestamp":1743040629225,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319489889"},{"type":"electronic","value":"9783319489896"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_13","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"199-216","source":"Crossref","is-referenced-by-count":0,"title":["Local Planning of Multiparty Interactions with Bounded Horizons"],"prefix":"10.1007","author":[{"given":"Mahieddine","family":"Dellabani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Combaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"13_CR1","unstructured":"Charette, R.N.: This car runs on code. IEEE Spectrum (2009)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Kopetz, H.: An integrated architecture for dependable embedded systems. In: Proceedings of the 23rd IEEE International Symposium on Reliable Distributed Systems, SRDS 2004, pp. 160\u2013161. IEEE Computer Society, Washington, DC (2004)","DOI":"10.1109\/RELDIS.2004.1353016"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Combaz, J., Sifakis, J.: Model-based implementation of real-time applications. In: EMSOFT (2010)","DOI":"10.1145\/1879021.1879052"},{"issue":"1","key":"13_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S1367-5788(03)00002-6","volume":"27","author":"H Kopetz","year":"2003","unstructured":"Kopetz, H.: Time-triggered real-time computing. Ann. Rev. Control 27(1), 3\u201313 (2003)","journal-title":"Ann. Rev. Control"},{"key":"13_CR5","unstructured":"Chabrol, D., David, V., Aussagu\u00e8s, C., Louise, S., Daumas, F.: Deterministic distributed safety-critical real-time systems within the oasis approach. In: International Conference on Parallel and Distributed Computing Systems, PDCS, 14\u201316 November 2005, Phoenix, AZ, USA, pp. 260\u2013268 (2005)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-24743-2_24","volume-title":"Hybrid Systems: Computation and Control","author":"A Ghosal","year":"2004","unstructured":"Ghosal, A., Henzinger, T.A., Kirsch, C.M., Sanvido, M.A.A.: Event-driven programming with logical execution times. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 357\u2013371. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24743-2_24"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kirsch, C.M., Matic, S.: Composable code generation for distributed giotto. In: Proceedings of the 2005 ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2005), 15\u201317 June 2005 Chicago, Illinois, USA, pp. 21\u201330 (2005)","DOI":"10.1145\/1065910.1065914"},{"key":"13_CR8","unstructured":"Behrmann, G., David, A., Guldstrand Larsen, K., H\u00e5kansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: QEST (2006)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Liu, J., Lee, E.A.: A programming model for time-synchronized distributed real-time systems. In: Proceedings of the 13th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, 3\u20136 April 2007, Bellevue, Washington, USA, pp. 259\u2013268 (2007)","DOI":"10.1109\/RTAS.2007.5"},{"issue":"9","key":"13_CR10","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1109\/32.31364","volume":"15","author":"R Bagrodia","year":"1989","unstructured":"Bagrodia, R.: Process synchronization: design and performance evaluation of distributed algorithms. IEEE Trans. Softw. Eng. 15(9), 1053\u20131065 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Bagrodia, R.: A distributed algorithm to implement n-party rendevouz. In: Proceedings Foundations of Software Technology and Theoretical Computer Science, Seventh Conference, Pune, India, 17\u201319 December 1987, pp. 138\u2013152 (1987)","DOI":"10.1007\/3-540-18625-5_48"},{"key":"13_CR12","volume-title":"Parallel Program Design: A Foundation","author":"K Mani Chandy","year":"1988","unstructured":"Mani Chandy, K., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co., Inc., Boston (1988)"},{"issue":"4","key":"13_CR13","doi-asserted-by":"crossref","first-page":"632","DOI":"10.1145\/1780.1804","volume":"6","author":"K Mani Chandy","year":"1984","unstructured":"Mani Chandy, K., Misra, J.: The drinking philosopher\u2019s problem. ACM Trans. Program. Lang. Syst. 6(4), 632\u2013646 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-46000-4_24","volume-title":"Coordination Models and Languages","author":"JA P\u00e9rez","year":"2002","unstructured":"P\u00e9rez, J.A., Corchuelo, R., Ruiz, D., Toro, M.: An order-based, distributed algorithm for implementing multiparty interactions. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol. 2315, pp. 250\u2013257. Springer, Heidelberg (2002). doi: 10.1007\/3-540-46000-4_24"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Parrow, J., Sj\u00f6din, P.: Multiway synchronizaton verified with coupled simulation. In: Proceedings of CONCUR \u201992, Third International Conference on Concurrency Theory, 24\u201327 August 1992, Stony Brook, NY, USA, pp. 518\u2013533 (1992)","DOI":"10.1007\/BFb0084813"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-15643-4_6","volume-title":"Automated Technology for Verification and Analysis","author":"S Bensalem","year":"2010","unstructured":"Bensalem, S., Bozga, M., Graf, S., Peled, D., Quinton, S.: Methods for knowledge based controlling of distributed systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 52\u201366. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15643-4_6"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-642-30793-5_8","volume-title":"Formal Techniques for Distributed Systems","author":"S Bensalem","year":"2012","unstructured":"Bensalem, S., Bozga, M., Quilbeuf, J., Sifakis, J.: Knowledge-based distributed conflict resolution for multiparty interactions and priorities. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 118\u2013134. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-30793-5_8"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-662-45234-9_13","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"S Bensalem","year":"2014","unstructured":"Bensalem, S., Bozga, M., Combaz, J., Triki, A.: Rigorous system design flow for autonomous systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8802, pp. 184\u2013198. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45234-9_13"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Triki, A.: Distributed Implementation of Timed Component-based Systems. Ph.D. thesis, UJF (2015)","DOI":"10.1109\/MEMCOD.2015.7340464"},{"key":"13_CR20","unstructured":"Saddek Bensalem Marius Bozga Mahieddine Dellabani, Jacques Combaz. Local planning of multiparty interactions with bounded horizon. Technical Report TR-2016-05, Verimag Research Report, 2016"},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR22","unstructured":"Tripakis, S.: The analysis of timed systems in practice. Ph.D. thesis, Joseph Fourier University (1998)"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-39893-6_28","volume-title":"Formal Methods and Software Engineering","author":"J Bengtsson","year":"2003","unstructured":"Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491\u2013503. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-39893-6_28"},{"key":"13_CR24","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"11","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 11, 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-54862-8_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L A\u015ftef\u0103noaei","year":"2014","unstructured":"A\u015ftef\u0103noaei, L., Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 263\u2013278. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54862-8_18"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Ben Rayana, S., Astefanoaei, L., Bensalem, S., Bozga, M., Combaz, J.: Compositional verification for timed systems based on automatic invariant generation. CoRR, abs\/1506.04879 (2015)","DOI":"10.2168\/LMCS-11(3:15)2015"},{"key":"13_CR27","unstructured":"Bensalem, M.B.S., Boyer, B., Legay, A.: Compositional invariant generation for timed systems. Technical report TR-2012-15, Verimag Research Report (2012)"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bozga, M., Boyer, B., Legay, A.: Incremental generation of linear invariants for component-based systems. In: 13th International Conference on Application of Concurrency to System Design (ACSD), pp. 80\u201389, July 2013","DOI":"10.1109\/ACSD.2013.11"},{"issue":"4","key":"13_CR29","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, Washington, DC, USA, pp. 3\u201312, IEEE Computer Society (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"13_CR31","unstructured":"Dutertre, B., de Moura, L.: The yices SMT solver. Technical report, SRI International (2006)"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188\u2013203. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_14"},{"issue":"1","key":"13_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1\u201311 (1987)","journal-title":"ACM Trans. Comput. Syst."},{"issue":"3","key":"13_CR34","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/s100090100048","volume":"3","author":"M Lindahl","year":"2001","unstructured":"Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gearbox controller. Springer Int. J. Softw. Tools Technol. Transf. (STTT) 3(3), 353\u2013368 (2001)","journal-title":"Springer Int. J. Softw. Tools Technol. Transf. (STTT)"}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,12]],"date-time":"2022-07-12T16:21:51Z","timestamp":1657642911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}