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.
Bernardeschi, C., Domenici, A., Fagiolini, A., Palmieri, M. (2023). Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications. COMPUTER JOURNAL, 66(2), 295-317 [10.1093/comjnl/bxab161].
Co-simulation and Formal Verification of Co-operative Drone Control With Logic-Based Specifications
Fagiolini, AdrianoPenultimo
;
2023-02-01
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.File | Dimensione | Formato | |
---|---|---|---|
bxab161 (1).pdf
accesso aperto
Tipologia:
Versione Editoriale
Dimensione
4.99 MB
Formato
Adobe PDF
|
4.99 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.