Paper Info
Title
CROME: Contract-Based Robotic Mission Specification
Abstract
We address the problem of automatically constructing a formal robotic mission specification in a logic language with precise semantics starting from an informal description of the mission requirements. We present CROME (Contract-based RObotic Mission spEcification), a framework that allows capturing mission requirements in terms of goals by using specification patterns, and automatically building linear temporal logic mission specifications conforming with the requirements. CROME leverages a new formal model, termed Contract-based Goal Graph (CGG), which enables organizing the requirements in a modular way with a rigorous compositional semantics. By relying on the CGG, it is then possible to automatically: i) check the feasibility of the overall mission, ii) further refine it from a library of pre-defined goals, and iii) synthesize multiple controllers that implement different parts of the mission at different abstraction levels, when the specification is realizable. If the overall mission is not realizable, CROME identifies mission scenarios, i.e., sub-missions that can be realizable. We illustrate the effectiveness of our methodology and supporting tool on a case study.
Year
DOI
Venue
2020
10.1109/MEMOCODE51338.2020.9315065
2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
Keywords
DocType
ISBN
CGG,contract-based robotic mission specification,contract-based goal graph,mission scenarios,linear temporal logic mission specifications,specification patterns,mission requirements,formal robotic mission specification,CROME
Conference
978-1-7281-9149-2
Citations 
PageRank 
References 
0
0.34
0
Authors
4
Name
Order
Citations
PageRank
Piergiuseppe Mallozzi1133.01
Pierluigi Nuzzo230533.35
Patrizio Pelliccione399884.04
Gerardo Schneider400.34