Formal verification of robotic behaviors in presence of bounded uncertainties

Julien Alexandre Dit Sandretto; Alexandre Chapoutot; Olivier Mullier

doi:10.1109/IRC.2017.17

Formal verification of robotic behaviors in presence of bounded uncertainties

Julien Alexandre Dit Sandretto, Alexandre Chapoutot, Olivier Mullier

ENSTA ParisTech

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Robotic behaviors are mainly described by differential equations. Those mathematical models are usually not precise enough because of inaccurately known parameters or model simplifications. Nevertheless, robots are often used in critical contexts as medical or military fields. So, uncertainties in mathematical models have to be taken into account in order to produce reliable and safe analysis results. A framework based on interval analysis is proposed to safely verify and analyze robotic behaviors with bounded uncertainties. It follows an interval constraint programming approach, combined with validated numerical integration methods to deal with differential equations. A case study on robust path planning is presented to emphasize the efficiency of the complete framework.

Original language	English
Title of host publication	Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	81-88
Number of pages	8
ISBN (Electronic)	9781509067237
DOIs	https://doi.org/10.1109/IRC.2017.17
Publication status	Published - 11 May 2017
Externally published	Yes
Event	1st IEEE International Conference on Robotic Computing, IRC 2017 - Taichung, Taiwan, Province of China Duration: 10 Apr 2017 → 12 Apr 2017

Publication series

Name	Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017

Conference

Conference	1st IEEE International Conference on Robotic Computing, IRC 2017
Country/Territory	Taiwan, Province of China
City	Taichung
Period	10/04/17 → 12/04/17

Keywords

Constraint satisfaction problems
Interval analysis
Validated numerical integration

Access to Document

10.1109/IRC.2017.17

Cite this

Sandretto, J. A. D., Chapoutot, A., & Mullier, O. (2017). Formal verification of robotic behaviors in presence of bounded uncertainties. In Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017 (pp. 81-88). Article 7926519 (Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/IRC.2017.17

Sandretto, Julien Alexandre Dit ; Chapoutot, Alexandre ; Mullier, Olivier. / Formal verification of robotic behaviors in presence of bounded uncertainties. Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017. Institute of Electrical and Electronics Engineers Inc., 2017. pp. 81-88 (Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017).

@inproceedings{3ae68e58b0e64159b97921bb5d24fbb2,

title = "Formal verification of robotic behaviors in presence of bounded uncertainties",

abstract = "Robotic behaviors are mainly described by differential equations. Those mathematical models are usually not precise enough because of inaccurately known parameters or model simplifications. Nevertheless, robots are often used in critical contexts as medical or military fields. So, uncertainties in mathematical models have to be taken into account in order to produce reliable and safe analysis results. A framework based on interval analysis is proposed to safely verify and analyze robotic behaviors with bounded uncertainties. It follows an interval constraint programming approach, combined with validated numerical integration methods to deal with differential equations. A case study on robust path planning is presented to emphasize the efficiency of the complete framework.",

keywords = "Constraint satisfaction problems, Interval analysis, Validated numerical integration",

author = "Sandretto, \{Julien Alexandre Dit\} and Alexandre Chapoutot and Olivier Mullier",

note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 1st IEEE International Conference on Robotic Computing, IRC 2017 ; Conference date: 10-04-2017 Through 12-04-2017",

year = "2017",

month = may,

day = "11",

doi = "10.1109/IRC.2017.17",

language = "English",

series = "Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "81--88",

booktitle = "Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017",

}

Sandretto, JAD , Chapoutot, A & Mullier, O 2017, Formal verification of robotic behaviors in presence of bounded uncertainties. in Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017., 7926519, Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017, Institute of Electrical and Electronics Engineers Inc., pp. 81-88, 1st IEEE International Conference on Robotic Computing, IRC 2017, Taichung, Taiwan, Province of China, 10/04/17. https://doi.org/10.1109/IRC.2017.17

Formal verification of robotic behaviors in presence of bounded uncertainties. / Sandretto, Julien Alexandre Dit ; Chapoutot, Alexandre; Mullier, Olivier.
Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017. Institute of Electrical and Electronics Engineers Inc., 2017. p. 81-88 7926519 (Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formal verification of robotic behaviors in presence of bounded uncertainties

AU - Sandretto, Julien Alexandre Dit

AU - Chapoutot, Alexandre

AU - Mullier, Olivier

PY - 2017/5/11

Y1 - 2017/5/11

N2 - Robotic behaviors are mainly described by differential equations. Those mathematical models are usually not precise enough because of inaccurately known parameters or model simplifications. Nevertheless, robots are often used in critical contexts as medical or military fields. So, uncertainties in mathematical models have to be taken into account in order to produce reliable and safe analysis results. A framework based on interval analysis is proposed to safely verify and analyze robotic behaviors with bounded uncertainties. It follows an interval constraint programming approach, combined with validated numerical integration methods to deal with differential equations. A case study on robust path planning is presented to emphasize the efficiency of the complete framework.

AB - Robotic behaviors are mainly described by differential equations. Those mathematical models are usually not precise enough because of inaccurately known parameters or model simplifications. Nevertheless, robots are often used in critical contexts as medical or military fields. So, uncertainties in mathematical models have to be taken into account in order to produce reliable and safe analysis results. A framework based on interval analysis is proposed to safely verify and analyze robotic behaviors with bounded uncertainties. It follows an interval constraint programming approach, combined with validated numerical integration methods to deal with differential equations. A case study on robust path planning is presented to emphasize the efficiency of the complete framework.

KW - Constraint satisfaction problems

KW - Interval analysis

KW - Validated numerical integration

U2 - 10.1109/IRC.2017.17

DO - 10.1109/IRC.2017.17

M3 - Conference contribution

AN - SCOPUS:85020175949

T3 - Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017

SP - 81

EP - 88

BT - Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 1st IEEE International Conference on Robotic Computing, IRC 2017

Y2 - 10 April 2017 through 12 April 2017

ER -

Sandretto JAD , Chapoutot A, Mullier O. Formal verification of robotic behaviors in presence of bounded uncertainties. In Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017. Institute of Electrical and Electronics Engineers Inc. 2017. p. 81-88. 7926519. (Proceedings - 2017 1st IEEE International Conference on Robotic Computing, IRC 2017). doi: 10.1109/IRC.2017.17

Formal verification of robotic behaviors in presence of bounded uncertainties

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this