Reference : Mind the gap: Robotic Mission Planning Meets Software Engineering
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/42896
Mind the gap: Robotic Mission Planning Meets Software Engineering
English
Askarpour, Mehrnoosh [Politecnico di Milano]
Menghi, Claudio mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Belli, Gabriele [Alten]
Bersani, Marcello [Politecnico di Milano]
Pelliccione, Patrizio [Chalmers | University of Gothenburg and University of L’Aquila]
2020
Proceedings of the 8th International Conference on Formal Methods in Software Engineering
Yes
International Conference on Formal Methods in Software Engineering (FormaliSE)
2020
[en] Planning ; Robotics ; Formal Methods ; Timed Automaton ; Temporal Logic ; Model Checking ; Uppaal
[en] In the context of robotic software, the selection of an appropriate planner is one of the most crucial software engineering decisions. Robot planners aim at computing plans (i.e., blueprint of actions) to accomplish a complex mission. While many planners have been proposed in the robotics literature, they are usually evaluated on showcase examples, making hard to understand whether they can be effectively (re)used for realising complex missions, with heterogeneous robots, and in real-world scenarios.
In this paper we propose ENFORCE, a framework which allows wrapping FM-based planners into comprehensive software engineering tools, and considers complex robotic missions. ENFORCE relies on (i) realistic maps (e.g, fire escape maps) that describe the environment in which the robots are deployed; (ii) temporal logic for mission specification; and (iii) Uppaal model checker to compute plans that satisfy mission specifications. We evaluated ENFORCE by analyzing how it supports computing plans in real case scenarios, and by evaluating the generated plans in simulated and real environments. The results show that while ENFORCE is adequate for handling single-robot applications, the state explosion still represents a major barrier for reusing existing planners in multi-robot applications.
http://hdl.handle.net/10993/42896
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Formalise.pdfAuthor postprint1.12 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.