{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T11:45:30Z","timestamp":1726055130698},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030322120"},{"type":"electronic","value":"9783030322137"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-32213-7_3","type":"book-chapter","created":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T23:04:57Z","timestamp":1571180697000},"page":"32-48","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On Reconciling Schedulability Analysis and Model Checking in Robotics"],"prefix":"10.1007","author":[{"given":"Mohammed","family":"Foughali","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,16]]},"reference":[{"key":"3_CR1","unstructured":"Robotnik Summit-XL data sheet. \n                    https:\/\/www.robotnik.eu\/web\/wp-content\/uploads\/\/2019\/03\/Robotnik_DATASHEET_SUMMIT-XL-HL_EN-web-1.pdf"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8\u201322. Springer, Heidelberg (1999). \n                    https:\/\/doi.org\/10.1007\/3-540-48683-6_3"},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2\u201334 (1993)","journal-title":"Inf. Comput."},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Amnell","year":"2004","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: a\u00a0tool for schedulability analysis and code generation of real-time systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 60\u201372. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-40903-8_6"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9 Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33\u201336. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-32759-9_6"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"issue":"14","key":"3_CR8","doi-asserted-by":"publisher","first-page":"2741","DOI":"10.1080\/00207540412331312688","volume":"42","author":"B Berthomieu","year":"2004","unstructured":"Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA-construction of abstract state spaces for Petri nets and time Petri nets. J. Prod. Res. 42(14), 2741\u20132756 (2004)","journal-title":"J. Prod. Res."},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-49213-5_5","volume-title":"Compositionality: The Significant Difference","author":"S Bornot","year":"1998","unstructured":"Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 103\u2013129. Springer, Heidelberg (1998). \n                    https:\/\/doi.org\/10.1007\/3-540-49213-5_5"},{"key":"3_CR10","unstructured":"D\u00edaz, J., et al.: Stochastic analysis of periodic real-time systems. In: RTSS, pp. 289\u2013300. IEEE (2002)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Foughali, M.: Toward a correct-and-scalable verification of concurrent robotic systems: insights on formalisms and tools. In: ACSD, pp. 29\u201338 (2017)","DOI":"10.1109\/ACSD.2017.10"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Foughali, M., Berthomieu, B., Dal Zilio, S., Hladik, P.-E., Ingrand, F., Mallet, A.: Formal verification of complex robotic systems on resource-constrained platforms. In: FormaliSE, pp. 2\u20139 (2018)","DOI":"10.1145\/3193992.3193996"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-47846-3_24","volume-title":"Formal Methods and Software Engineering","author":"M Foughali","year":"2016","unstructured":"Foughali, M., Berthomieu, B., Dal Zilio, S., Ingrand, F., Mallet, A.: Model checking real-time properties on the functional layer of autonomous robots. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 383\u2013399. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-47846-3_24"},{"key":"3_CR14","unstructured":"Foughali, M., Dal Zilio, S., Ingrand, F.: On the Semantics of the GenoM3 Framework. Technical report (2019)"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Foughali, M., Ingrand, F., Seceleanu, C.: Statistical model checking of complex robotic systems. In: SPIN (2019)","DOI":"10.1007\/978-3-030-30923-7_7"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Gobillot, N., Guet, F., Doose, D., Grand, C., Lesire, C., Santinelli, L.: Measurement-based real-time analysis of robotic software architectures. In: IROS, pp. 3306\u20133311. IEEE (2016)","DOI":"10.1109\/IROS.2016.7759509"},{"key":"3_CR17","unstructured":"Goddard, S., Huang, J., Farritor, S., et al.: A performance and schedulability analysis of an autonomous mobile robot. In: ECRTS, pp. 239\u2013248. IEEE (2005)"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T Henzinger","year":"1994","unstructured":"Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"issue":"2","key":"3_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s11334-011-0152-5","volume":"7","author":"X Huang","year":"2011","unstructured":"Huang, X., Singh, A., Smolka, S.: Using integer clocks to verify clock-synchronization protocols. Innov. Syst. Softw. Eng. 7(2), 119\u2013130 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"3_CR20","unstructured":"Kargahi, M., Movaghar, A.: Non-preemptive earliest-deadline-first scheduling policy: a performance study. In: MASCOTS, pp. 201\u2013208. IEEE (2005)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11562948_32","volume-title":"Automated Technology for Verification and Analysis","author":"M Kim","year":"2005","unstructured":"Kim, M., Kang, K.C.: Formal construction and verification of home service robots: a case study. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 429\u2013443. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/11562948_32"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54\u201357. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Mallet, A., Pasteur, C., Herrb, M., Lemaignan, S., Ingrand, F.: GenoM3: building middleware-independent robotic components. In: ICRA, pp. 4627\u20134632. IEEE (2010)","DOI":"10.1109\/ROBOT.2010.5509539"},{"issue":"9","key":"3_CR24","doi-asserted-by":"publisher","first-page":"1036","DOI":"10.1109\/TCOM.1976.1093424","volume":"24","author":"P Merlin","year":"1976","unstructured":"Merlin, P., Farber, D.: Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE Transactions on Communications 24(9), 1036\u20131043 (1976)","journal-title":"IEEE Transactions on Communications"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J.: Automatic property checking of robotic applications. In: IROS, pp. 3869\u20133876. IEEE (2017)","DOI":"10.1109\/IROS.2017.8206238"},{"issue":"2","key":"3_CR26","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1080\/095281300409856","volume":"12","author":"M Piaggio","year":"2000","unstructured":"Piaggio, M., Sgorbissa, A., Zaccaria, R.: Pre-emptive versus non-pre-emptive real time scheduling in intelligent mobile robotics. J. Exp. Theor. Artif. Intell. 12(2), 235\u2013245 (2000)","journal-title":"J. Exp. Theor. Artif. Intell."},{"key":"3_CR27","unstructured":"Sensfelder, N., Brunel, J., Pagetti, C.: Modeling cache coherence to expose interference. In: ECRTS (2019)"},{"key":"3_CR28","unstructured":"Shi, J., Goddard, S., Lal, A., Farritor, S.: A real-time model for the robotic highway safety marker system. In: RTAS, pp. 331\u2013340. IEEE (2004)"},{"key":"3_CR29","unstructured":"Shih, C., Sha, L., Liu, J.: Scheduling tasks with variable deadlines. In: RTAS, pp. 120\u2013122. IEEE (2001)"},{"issue":"5","key":"3_CR30","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S1571-0661(05)80435-9","volume":"65","author":"A Sowmya","year":"2002","unstructured":"Sowmya, A., Tsz-Wang So, D., Hung Tang, W.: Design of a mobile robot controller using Esterel tools. Electron. Not. Theor. Comput. Sci. 65(5), 3\u201310 (2002)","journal-title":"Electron. Not. Theor. Comput. Sci."}],"container-title":["Communications in Computer and Information Science","New Trends in Model and Data Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32213-7_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T23:06:06Z","timestamp":1571180766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32213-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030322120","9783030322137"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32213-7_3","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"16 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MEDI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model and Data Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"medi2019a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.irit.fr\/MEDI2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Peer Review Information from Medi International Workshops (DETECT, DSSGA and TRIDENT): out of 34 submissions and 1 invited paper, 13 full papers and 3 short papers were accepted","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}