APPLICATION OF PROPERTY PROVING TO QUADCOPTER FLIGHT CONTROL SOFTWARE

D. V. Sokol, A. B. Zhukevych, H. A. Miroshnychenko

Abstract


The object of the study is a computer model of an automatic control system for a quadcopter. The subject matter of the research encompasses the application of formal methods for analyzing and verifying requirements for quadcopter control systems, with a particular focus on the capabilities of the Simulink Design Verifier™ tool. The primary goal of the study is to enhance the overall reliability of the quadcopter model by applying formal analysis techniques at the design stage to uncover potential logical and structural errors before physical implementation. The tasks to be solved: conducting a comprehensive review of challenges associated with the operation of commercial quadcopter platforms; formulating safety-oriented requirements for quadcopter flight control; developing a detailed simulation model of the control system using the Simulink® environment; utilizing the Property Proving functionality to perform formal verification of critical system properties; analyzing and interpreting the verification reports generated by the tool; and identifying latent design flaws or inconsistencies that may compromise system safety. The study employed the following methods: formal verification using the Property Proving tool, simulation-based modeling, static code analysis, and model-based testing. As a result of the research, it was demonstrated how formal verification techniques, such as Property Proving, can be applied to validate safety-critical behaviors of quadcopter control systems. The use of Simulink Design Verifier™ proved effective in identifying design weaknesses early in the development cycle, reducing downstream risk and rework. Additionally, the generation of interactive diagnostic reports facilitated the visualization of failure scenarios and supported iterative debugging. Conclusions. The application of formal analysis tools such as Simulink Design Verifier™ represents a valuable approach to strengthening quadcopter control system reliability, if models are properly constructed and properties are carefully defined. Although limitations exist – particularly concerning compatibility with certain Simulink® blocks – the tool remains a powerful complement to traditional testing, especially when addressing high-assurance system requirements. The study underscores the necessity of integrating formal methods into standard verification workflows to balance theoretical rigor with practical validation.


Keywords


UAV; quadcopter; control system; design; static analysis; property proving; computer model.

Full Text:

PDF

References


Fedorovich, O., Krytskyi, D., Lukhanin, M., Prokho-rov, O., & Leshchenko, Y. Modeling of strike drone missions for conducting wave attacks in conditions of enemy anti-drone actions. Radioelectronic and Computer Systems, 2025, vol. 2025, no, 1, pp. 29-43. DOI: 10.32620/reks.2025.1.02.

Pogudin, A., Pohudina, O., Bykov, A., & Plastun, T. Simulation of the automatic flight of a small unmanned aerial vehicle over a marker line. Open Information and Computer Integrated Technologies, 2022, no. 95, pp. 71-82. DOI: 10.32620/oikit.2022.95.06.

Xiao W. SRAD: Autonomous Decision-Making Method for UAV Based on Safety Reinforcement Learning / W. Xiao, X. Luo, S. Xie // Expert Systems. – 2025. – Vol. 42, Iss. 5. – 18 p. DOI: 10.1111/exsy.70004.

Ma B. Safety flight envelope calculation and protection control of UAV based on disturbance observer / B. Ma, M. Chen // Security and Safety. – 2023. – Vol. 2(2023020). – 17 p. DOI: 10.1051/sands/2023020.

Hung I.-K. Assessing Drone Return-to-Home Landing Accuracy in a Woodland Landscape / I.-K. Hung, D. Unger, Y. Zhang, D. Kulhavy // Drones and Autonomous Vehicles. – 2024. – Vol. 1(3). DOI: 10.35534/dav.2024.10005.

Shcherban A. UAV Flight Safety System Based on Fuzzy Logic /A. Shcherban, V. Ieremenko // Transactions on Aerospace Research. – 2020. –Vol. 4. – P. 71–80. DOI: 10.2478/tar-2020-0022.

Motwakela A. Fuzzy logic in real-time decision making for autonomous drones / A. Motwakela et al. // International Journal of Data and Network Science. – 2024. – Vol. 9, Iss. 2. – P. 335–344. DOI: 10.5267/j.ijdns.2024.7.008.

Shcherban A. Validating Lithium-Polymer Battery Discharge Models to Ensure UAV Flight Safety and Performance/ A. Shcherban, V. Eremenko // Transactions on Aerospace Research. – 2024. – Vol. 4. – P. 80–100. DOI: 10.2478/tar-2024-0024.

Trauth M. H. Introduction to MATLAB. In: MATLAB® Recipes for Earth Sciences / M. H. Trauth // Springer Textbooks in Earth Sciences, Geography and Environment / Springer, Cham. – 2025. – 567 p. DOI: 10.1007/978-3-031-57949-3_2.

What Is Property Proving? / The MathWorks, Inc., 2024. – https://www.mathworks.com/help/sldv/ug/what-is-property-proving.html (23.04.2025).

Zhukevych A. Study of mutual influence between control channels of the quadcopter due to the low maneuverability of the UAV / A. Zhukevych, V. Dzhulgakov, O. Zhukevych // Aerospace technic and technology. – 2022. – Vol. 5, Iss. 183. – P. 68–81. DOI: 10.32620/aktt.2022.5.06.

Supported and Unsupported Simulink Blocks in Simulink Design Verifier / The MathWorks, Inc., 2024. – https://www.mathworks.com/help/sldv/ug/simulink-block-support.html (23.04.2025).

Yorkston K. Performance Testing. An ISTQB Certified Tester Foundation Level Specialist Certification Review / K. Yorkston // Apress Berkeley, CA. – 2021. – 394 p. DOI: 10.1007/978-1-4842-7255-8.




DOI: https://doi.org/10.32620/oikit.2025.104.12

Refbacks

  • There are currently no refbacks.