,
,
,
, > start {guard pi_<
, >_exec {guard 14 <' if {$c in $p} {'> 15 pi_<, > && 16 <' }'>!( 17 <' foreach m
,
, References 1. The PocoLibs middleware
, 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
, The Esterel v5 language primer: version v5 91. Centre de mathématiques appliquées, Ecole des mines and INRIA, 2000.
, 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
, 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
, 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
, 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
, 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
, 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
, 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
, On the Semantics of the GenoM3 Framework, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01992470
, GOLEX --bridging the gap between logic (GOLOG) and a real robot, Annual Conference on Artificial Intelligence, pp.165-176, 1998.
, 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
, Testing, verification and improvements of timeliness in ROS processes, Annual Conference Towards Autonomous Robotic Systems (TAROS), pp.146-157, 2016.
, Timed transition systems, Research and Education in Concurrent Systems, pp.226-251, 1991.
, 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
, 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
, 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.
, Correct, reactive, high-level robot control, IEEE Robotics & Automation Magazine, vol.18, issue.3, pp.65-74, 2011.
DOI : 10.1109/mra.2011.942116
, 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
, Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol, Formal Aspects of Computing, vol.14, pp.295-318, 2003.
, 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
, GenoM3: Building middleware-independent robotic components, International Conference on Robotics and Automation (ICRA), pp.4627-4632, 2010.
DOI : 10.1109/robot.2010.5509539
, Automatic property checking of robotic applications, International Conference on Intelligent Robots and Systems (IROS), pp.3869-3876, 2017.
, Verification and validation of autonomy software at NASA, 2000.
, ROS: an open-source Robot Operating System, ICRA workshop on open source software, 2009.
, Understanding concurrent systems, 2010.
DOI : 10.1007/978-1-84882-258-0
, 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
, Behavior verification of autonomous robot vehicle in consideration of errors and sisturbances, International Computer Software and Applications Conference (COMPSAC), pp.550-555, 2015.
, 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
, Design of a mobile robot controller using Esterel tools, Electronic Notes in Theoretical Computer Science, vol.65, issue.5, pp.3-10, 2002.
, Designing a secure and robust mobile interacting robot for the long term, International Conference on Robotics and Automation (ICRA), pp.4246-4251, 2003.
, The CLARAty architecture for robotic autonomy, Aerospace Conference, pp.1-121, 2001.
DOI : 10.1109/aero.2001.931701