Contract-Based Specification Refinement and Repair for Mission Planning
We address the problem of modeling, refining, and repairing formal specifications for robotic missions using assume-guarantee contracts. We show how to model mission specifications at various levels of abstraction and implement them using a library of pre-implemented specifications. Suppose the specification cannot be met using components from the library. In that case, we compute a proxy for the best approximation to the specification that can be generated using elements from the library. Afterward, we propose a systematic way to either 1) search for and refine the `missing part’ of the specification that the library cannot meet or 2) repair the current specification such that the existing library can refine it. Our methodology for searching and repairing mission requirements leverages the quotient, separation, composition, and merging operations between contracts.
Sun 14 MayDisplayed time zone: Hobart change
13:45 - 15:15 | SpecificationFormaliSE 2023 at Meeting Room 102 Chair(s): Larissa A. Meinicke The University of Queensland | ||
13:45 30mPaper | Contract-Based Specification Refinement and Repair for Mission Planning FormaliSE 2023 Piergiuseppe Mallozzi UC Berkeley, Inigo Incer University of California, Berkeley, Pierluigi Nuzzo University of Southern California, Alberto L. Sangiovanni-Vincentelli University of California at Berkeley, USA | ||
14:15 30mPaper | Patch Specifications via Product Programs FormaliSE 2023 Cristian Cadar Imperial College London, UK, Daniel Schemmel Imperial College London, Arindam Sharma Imperial College London | ||
14:45 30mPaper | An Empirical Study Assessing Software Modeling in Alloy FormaliSE 2023 Niloofar Mansoor University of Nebraska-Lincoln, Hamid Bagheri University of Nebraska-Lincoln, Eunsuk Kang Carnegie Mellon University, Bonita Sharif University of Nebraska-Lincoln, USA | ||