Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications. (23rd October 2021)

• Record Type: Journal Article
• Authors: Bernardeschi, Cinzia; Domenici, Andrea; Fagiolini, Adriano; Palmieri, Maurizio
• Is Part Of: Computer journal. Volume 66:Number 2(2023)
• Page Start: 295
• Page End: 317
• Publication Date: 2021-10-23
• Subjects: formal methods -- co-operative control -- co-simulation -- verification -- theorem prover; Computers -- Periodicals; 005.1
• DOI: 10.1093/comjnl/bxab161
• Languages: English
• ISSNs: 0010-4620

Abstract

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.