Our evaluation addressed the following two questions.
RQ1: How effective is the pattern catalog in capturing mission requirements and producing mission specifications?
RQ2: Are the proposed mission specifications correct?
Coverage of Real-World Missions (RQ1)
We investigated (i) how the pattern catalog supports the specification of mission requirements and (ii) how the pattern catalog reduces ambiguities in mission requirements.
We checked how the pattern catalog supports the formulation of mission requirements (and the generation of mission specifications) in real-world robotic scenarios. To this end, we defined five scenarios in collaboration with our industrial partners. See more on the Experiment 1 dedicated page.
We collected mission requirements in natural language from available requirements produced from Spectra and LTLMoP. We checked how the pattern catalog may have supported developers in the definition of the mission requirements. See more on the Experiment 2 dedicated page.
We analyzed the mission specifications contained in the Spectra examples collected in Exp2. We collected 1216 distinct LTL mission specifications and we analyzed each of these specifications. We verified whether it is possible to obtain the mission specifications starting from the proposed patterns. See more on the Experiment 3 dedicated page.
Correctness of the Patterns (RQ2)
We generated the LTL specifications of the considered mission requirements. We (i) negated the LTL specification; (ii) encoded the specification and the model of the scenario in NuSMV ; (iii) used NuSMV to check whether the models contained a path that satisfied the mission specification (violates its negation). We also checked the correctness of the generated plans using the Simbad simulator. See more on the Experiment 4 dedicated page.
We generated LTL and CTL specifications for the considered mission requirements. We (i) encoded the LTL and CTL specifications and the model of the scenario in NuSMV; (iii) we used NuSMV to check whether the verification of the specifications returned the same results. See more on the Experiment 5 dedicated page.
We investigated why in several cases the mission requirement was always not satisfied. In these cases we relaxed the mission requirements, by removing certain patterns. We executed the same steps of Exp4. See more on the Experiment 6 dedicated page.