1. Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
- Author
-
Adriano Fagiolini, Maurizio Palmieri, Andrea Domenici, Cinzia Bernardeschi, Bernardeschi, Cinzia, Domenici, Andrea, Fagiolini, Adriano, and Palmieri, Maurizio
- Subjects
Co operative ,formal methods ,General Computer Science ,theorem prover ,Computer science ,Control (management) ,formal methods, co-operative control, co-simulation, verification, theorem prover ,Co-simulation ,Drone ,co-operative control ,Settore ING-INF/04 - Automatica ,formal method ,co-simulation ,verification ,Formal verification ,Simulation - Abstract
Unmanned aerial vehicle (UAV) co-operative systems are complex cyber-physical systems that integrate a high-level control algorithm with pre-existing closed implementations of lower-level vehicle kinematics. In model-driven development, simulation is one of the techniques that are usually applied, together with testing, in the analysis of system behaviours. This work proposes a method and tools to validate the design of UAV co-operative systems based on co-simulation and formal verification. The method uses the Prototype Verification System, an interactive theorem prover based on a higher-order logic language, and the Functional Mock-up Interface, a widely accepted standard for co-simulation. In this paper, results on the co-simulation and proofs of safety requirements of a representative co-ordination algorithm are shown and discussed in a scenario where quadcopters are deployed and perform space-coverage operations.
- Published
- 2023