R. Alur, Timed automata, proc. of the International Conference on Computer Aided Verification, CAV, pp.8-22, 1999.

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.

R. Alur, C. Courcoubetis, and D. L. Dill, Model-checking in dense real-time. Information and computation, vol.104, pp.2-34, 1993.

T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi, TIMES: a tool for schedulability analysis and code generation of real-time systems, Proc. of the International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS, pp.60-72, 2003.

É. André, L. Fribourg, U. Kühne, and R. Soulat, Imitator 2.5: A tool for analyzing robustness in scheduling problems, Proc. of the International Symposium on Formal Methods, FM, pp.33-36, 2012.

G. Behrmann, A. David, and K. G. Larsen, A tutorial on UPPAAL, Proc. of the Formal Methods for the Design of Real-Time Systems, SFM-RT, pp.200-236, 2004.

G. Bernat, A. Burns, and A. Liamosi, Weakly hard real-time systems, IEEE transactions on Computers, vol.50, issue.4, pp.308-321, 2001.

B. Berthomieu, P. Ribet, and F. Vernadat, The tool TINA -construction of abstract state spaces for Petri nets and time Petri nets, International Journal of Production Research, vol.42, issue.14, pp.2741-2756, 2004.

S. Bornot, J. Sifakis, and S. Tripakis, Modeling urgency in timed systems, Proc. of the International Symposium on Compositionality, COMPOS, pp.103-129, 1998.

F. Cicirelli, A. Furfaro, L. Nigro, and F. Pupo, Development of a schedulability analysis framework based on ptpn and uppaal with stopwatches, Proc. of the IEEE/ACM 16th International Symposium on Distributed Simulation and Real Time Applications, DS-RT, pp.57-64, 2012.

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, NuSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.410-425, 2000.

M. Cordovilla, F. Boniol, E. Noulard, and C. Pagetti, Multiprocessor schedulability analyser, Proc. of the ACM Symposium on Applied Computing, SAC, pp.735-741, 2011.

A. David, J. I. Rasmussen, K. G. Larsen, and A. Skou, Model-based Framework for Schedulability Analysis Using Uppaal 4.1, pp.93-119, 2009.

R. I. Davis and A. Burns, A survey of hard real-time scheduling for multiprocessor systems, ACM Computer Survey, vol.43, issue.4, 2011.

J. Louis-díaz, D. García, K. Kim, C. Lee, L. L. Bello et al., Stochastic analysis of periodic real-time systems, Proc of the IEEE Real-Time Systems Symposium, RTSS, pp.289-300, 2002.

M. Foughali, Formal Verification of the Functional Layer of Robotic and Autonomous Systems, 2018.

M. Foughali, On reconciling schedulability analysis and model checking in robotics, Proc. of International Conference on Model and Data Engineering, pp.32-48, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02346015

M. Foughali, B. Berthomieu, S. D. Zilio, F. Ingrand, and A. Mallet, Model checking real-time properties on the functional layer of autonomous robots, Proc. of the International Conference on Formal Engineering Methods, ICFEM, pp.383-399, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01346080

M. Foughali, B. Berthomieu, S. D. Zilio, P. Hladik, F. Ingrand et al., Formal verification of complex robotic systems on resource-constrained platforms, Proc. of the Conference on Formal Methods in Software Engineering, FormaliSE, pp.2-9, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01778960

M. Foughali, S. D. Zilio, and F. Ingrand, On the Semantics of the GenoM3 Framework, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01992470

M. Foughali, F. Ingrand, and C. Seceleanu, Statistical model checking of complex robotic systems, Proc. of the International Symposium on Model Checking Software, SPIN, pp.114-134, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02152286

N. Gobillot, C. Lesire, and D. Doose, A design and analysis methodology for component-based real-time architectures of autonomous systems, Journal of Intelligent & Robotic Systems, vol.96, issue.1, pp.123-138, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02467969

N. Guan, Z. Gu, M. Lv, Q. Deng, and G. Yu, Schedulability analysis of global fixed-priority or EDF multiprocessor scheduling with symbolic model-checking, Proc. of the 11th IEEE Symposium on Object Oriented Real-Time Distributed Computing, ISORC, pp.556-560, 2008.

T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, Information and computation, vol.111, issue.2, pp.193-244, 1994.

T. Henzinger, P. Ho, and H. Wong-toi, HyTech: A model checker for hybrid systems, Proc. of the International Conference on Computer Aided Verification, pp.460-463, 1997.

X. Huang, A. Singh, and S. A. Smolka, Using integer clocks to verify clock-synchronization protocols, Innovations in Systems and Software Engineering, vol.7, pp.119-130, 2011.

M. Kargahi and A. Movaghar, Non-preemptive earliest-deadline-first scheduling policy: A performance study, Proc. of the IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, MASCOTS, pp.201-208, 2005.

M. Kim and K. Kang, Formal Construction and Verification of Home Service Robots: A Case Study, Proc. of the International Symposium on Automated Technology for Verification and Analysis, pp.429-443, 2005.

K. Lakshmanan, R. Dionisio-de-niz, G. Rajkumar, and . Moreno, Resource allocation in distributed mixed-criticality cyber-physical systems, Proc. of the International Conference on Distributed Computing Systems, ICDCS, pp.169-178, 2010.

I. Lee, Y. Joseph, S. H. Leung, and . Son, Handbook of Real-Time and Embedded Systems, p.9781584886785, 2007.

D. Lime and O. H. Roux, Formal verification of real-time systems with preemptive scheduling. Real-Time Systems, vol.41, pp.118-151, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00453476

D. Lime, H. Olivier, C. Roux, L. Seidner, . Traonouez et al., A parametric model-checker for Petri nets with stopwatches, Proc. of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, pp.54-57, 2009.

C. Liu, H. James, and . Anderson, Suspension-aware analysis for hard real-time multiprocessor scheduling, Proc. of the Euromicro Conference on Real-Time Systems, ECRTS, pp.271-281, 2013.

P. Merlin and D. Farber, Recoverability of Communication Protocols: Implications of a Theoretical Study, IEEE Transactions on Communications, vol.24, issue.9, pp.1036-1043, 1976.

A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, and J. Timmis, Automatic property checking of robotic applications, Proc. of the International Conference on Intelligent Robots and Systems, IROS, pp.3869-3876, 2017.

L. Molnar and S. Veres, System verification of autonomous underwater vehicles by model checking, Proc. of the OCEANS-EUROPE Conference, pp.1-10, 2009.

M. Nasri, I. Robert, . Davis, B. Björn, and . Brandenburg, FIFO with offsets: High schedulability with low overheads, Proc. of the Real-Time and Embedded Technology and Applications Symposium, pp.271-282, 2018.

F. Peres, P. Hladik, and F. Vernadat, Specification and verification of real-time systems using POLA, International Journal of Critical Computer-Based Systems, vol.2, issue.3-4, pp.332-351, 2011.

M. Piaggio, A. Sgorbissa, and R. Zaccaria, Pre-emptive versus non-pre-emptive real time scheduling in intelligent mobile robotics, Journal of Experimental & Theoretical Artificial Intelligence, vol.12, issue.2, pp.235-245, 2000.

S. Qadi, A. Goddard, J. Huang, and S. Farritor, A performance and schedulability analysis of an autonomous mobile robot, Proc. of the IEEE Euromicro Conference on Real-Time Systems, ECRTS, pp.239-248, 2005.

C. Ramchandani, Analysis of asynchronous concurrent systems by Petri nets, 1974.

N. Sensfelder, J. Brunel, and C. Pagetti, Modeling cache coherence to expose interference, Proc. of the IEEE Euromicro Conference on Real-Time Systems, ECRTS. IEEE, 2019.

W. Sheng, Y. Gao, L. Xi, and X. Zhou, Schedulability analysis for multicore global scheduling with model checking, Proc. of the 11th International Workshop on Microprocessor Test and Verification, pp.21-26, 2010.

J. Shi, S. Goddard, A. Lal, and S. Farritor, A real-time model for the robotic highway safety marker system, Proc. of the IEEE Real-Time and Embedded Technology and Applications Symposium, pp.331-340, 2004.

C. Shih, L. Sha, and J. Liu, Scheduling tasks with variable deadlines, Proc. of the IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, pp.120-122, 2001.

M. Short, On the implementation of dependable real-time systems with nonpreemptive edf, Electrical Engineering and Applied Computing, vol.20, 2011.

D. Simon, R. Pissard-gibollet, and S. Arias, Orccad, a framework for safe robot control design and implementation, Proc. of the Workshop on Control Architectures of Robots: software approaches and issues, CAR, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00385258

L. Waszniowski and Z. Hanzálek, Formal verification of multitasking applications based on timed automata model. Real-Time Systems, vol.38, pp.39-65, 2008.

B. Yalcinkaya, M. Nasri, and B. B. Brandenburg, An exact schedulability test for non-preemptive self-suspending real-time tasks, Proc. of the Design, Automation Test in Europe Conference Exhibition, DATE, pp.1228-1233, 2019.