&. ,

&. ,

&. ,

, > start {guard pi_<

&. , >_exec {guard 14 <' if {$c in $p} {'> 15 pi_<, > && 16 <' }'>!( 17 <' foreach m

. &lt;&apos;-if-{$m-!=-;-}-{&apos;&gt;-||-&lt;&apos;-}&apos;&gt;,

, References 1. The PocoLibs middleware

G. Behrmann, A. David, and K. G. Larsen, A tutorial on UPPAAL, Formal Methods for the Design of Real-Time Systems, pp.200-236, 2004.
DOI : 10.1007/978-3-540-30080-9_7

G. Berry, The Esterel v5 language primer: version v5 91. Centre de mathématiques appliquées, Ecole des mines and INRIA, 2000.

S. Bornot, J. Sifakis, and S. Tripakis, Modeling urgency in timed systems, International Symposium on Compositionality (ISC): the significant difference, pp.103-129, 1998.
DOI : 10.1007/3-540-49213-5_5

P. Bulychev, A. David, K. Larsen, A. Legay, G. Li et al., Monitorbased statistical model checking for weighted metric temporal logic, International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), pp.168-182, 2012.
DOI : 10.1007/978-3-642-28717-6_15

URL : https://hal.archives-ouvertes.fr/hal-00744100

Q. Cappart, C. Limbrée, P. Schaus, J. Quilbeuf, L. Traonouez et al., Verification of interlocking systems using statistical model checking, 2017 IEEE 18th International Symposium on High Assurance Systems Engineering (HASE), pp.61-68, 2017.
DOI : 10.1109/hase.2017.10

URL : https://hal.archives-ouvertes.fr/hal-01398649

A. Cimatti, M. Roveri, and P. Bertoli, Conformant planning via symbolic model checking and heuristic search, Artificial Intelligence, vol.159, issue.1-2, pp.127-206, 2004.
DOI : 10.1016/j.artint.2004.05.003

URL : https://doi.org/10.1016/j.artint.2004.05.003

M. Foughali, Toward a Correct-and-Scalable Verification of Concurrent Robotic Systems: Insights on Formalisms and Tools, International Conference on Application of Concurrency to System Design (ACSD), pp.29-38, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01515012

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

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

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

D. Hähnel, W. Burgard, and G. Lakemeyer, GOLEX --bridging the gap between logic (GOLOG) and a real robot, Annual Conference on Artificial Intelligence, pp.165-176, 1998.

R. Halder, J. Proença, N. Macedo, and A. Santos, Formal verification of ROS-based robotic applications using timed-automata, International Conference on Formal Methods in Software Engineering (FormaliSE), p.2017
DOI : 10.1109/formalise.2017.9

URL : http://repositorio.inesctec.pt/bitstream/123456789/5582/1/P-00M-YNE.pdf

M. Hazim, H. Qu, and S. Veres, Testing, verification and improvements of timeliness in ROS processes, Annual Conference Towards Autonomous Robotic Systems (TAROS), pp.146-157, 2016.

T. Henzinger, Z. Manna, and A. Pnueli, Timed transition systems, Research and Education in Concurrent Systems, pp.226-251, 1991.

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.
DOI : 10.1006/inco.1994.1045

URL : https://doi.org/10.1006/inco.1994.1045

F. Ingrand and M. Ghallab, Deliberation for autonomous robots: A survey, Artificial Intelligence, vol.247, pp.10-44, 2017.
DOI : 10.1016/j.artint.2014.11.003

URL : https://hal.archives-ouvertes.fr/hal-01137921

M. Kim and K. Kang, Formal construction and verification of home service robots: A case study, International Symposium on Automated Technology for Verification and Analysis (ATVA), pp.429-443, 2005.

H. Kress-gazit, T. Wongpiromsarn, and U. Topcu, Correct, reactive, high-level robot control, IEEE Robotics & Automation Magazine, vol.18, issue.3, pp.65-74, 2011.
DOI : 10.1109/mra.2011.942116

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of probabilistic realtime systems, International Conference on Computer-Aided Verification (CAV), pp.585-591, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol, Formal Aspects of Computing, vol.14, pp.295-318, 2003.

A. Legay, B. Delahaye, and S. Bensalem, Statistical model checking: An overview, International Conference on Runtime Verification (RV), pp.122-135, 2010.
DOI : 10.1007/978-3-642-16612-9_11

URL : https://hal.archives-ouvertes.fr/inria-00591593

A. Mallet, C. Pasteur, M. Herrb, S. Lemaignan, and F. Ingrand, GenoM3: Building middleware-independent robotic components, International Conference on Robotics and Automation (ICRA), pp.4627-4632, 2010.
DOI : 10.1109/robot.2010.5509539

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

C. Pecheur, Verification and validation of autonomy software at NASA, 2000.

M. Quigley, B. Gerkey, K. Conley, J. Faust, T. Foote et al., ROS: an open-source Robot Operating System, ICRA workshop on open source software, 2009.

A. Roscoe, Understanding concurrent systems, 2010.
DOI : 10.1007/978-1-84882-258-0

C. Seceleanu, A. Vulgarakis, and P. Pettersson, REMES: A resource model for embedded systems, International Conference on Engineering of Complex Computer Systems (ICECCS), pp.84-94, 2009.
DOI : 10.1109/iceccs.2009.49

T. Sekizawa, F. Otsuki, K. Ito, and K. Okano, Behavior verification of autonomous robot vehicle in consideration of errors and sisturbances, International Computer Software and Applications Conference (COMPSAC), pp.550-555, 2015.

D. Simon, R. Pissard-gibollet, and S. Arias, Orccad, a framework for safe robot control design and implementation, National workshop on control architectures of robots: software approaches and issues (CAR), 2006.
URL : https://hal.archives-ouvertes.fr/inria-00385258

A. Sowmya, D. Tsz, -. So, and W. H. Tang, Design of a mobile robot controller using Esterel tools, Electronic Notes in Theoretical Computer Science, vol.65, issue.5, pp.3-10, 2002.

N. Tomatis, G. Terrien, R. Piguet, D. Burnier, S. Bouabdallah et al., Designing a secure and robust mobile interacting robot for the long term, International Conference on Robotics and Automation (ICRA), pp.4246-4251, 2003.

R. Volpe, I. Nesnas, T. Estlin, D. Mutz, R. Petras et al., The CLARAty architecture for robotic autonomy, Aerospace Conference, pp.1-121, 2001.
DOI : 10.1109/aero.2001.931701