6533b827fe1ef96bd1286656
RESEARCH PRODUCT
Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
Adriano FagioliniMaurizio PalmieriAndrea DomeniciCinzia Bernardeschisubject
Co operativeformal methodsGeneral Computer Sciencetheorem proverComputer scienceControl (management)formal methods co-operative control co-simulation verification theorem proverCo-simulationDroneco-operative controlSettore ING-INF/04 - Automaticaformal methodco-simulationverificationFormal verificationSimulationdescription
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.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2021-10-23 |