Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
| Autor: | Adriano Fagiolini, Maurizio Palmieri, Andrea Domenici, Cinzia Bernardeschi |
|---|---|
| Přispěvatelé: | Bernardeschi, Cinzia, Domenici, Andrea, Fagiolini, Adriano, Palmieri, Maurizio |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: |
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 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|