Designing robust quadcopter software based on a real-time partitioned operating system and formal verification techniques

The creation of reliable unmanned aerial vehicles (drones) now is an important task in the science and technology, because such devices can have a lot of use-cases in the digital economy and modern life, so we need to ensure the reliability here. In this article, it is proposed to assemble a quadcopter from low-cost components in order to obtain a hardware prototype and to develop a software solution for the flight controller with high-reliability requirements, which will meet avionics software standards using existing open-source software solutions, and also apply the results as a model for teaching courses “Components of operating systems” and “Software verification”. In the study, we proceed to analyse the structure of quadcopters and flight controllers for them, represent a self-assembly solution. We describe Ardupilot as open-source software for unmanned aerial vehicles, the appropriate APM controller and methods of PID control. Today's avionics standard of reliable software for flight controllers is a real-time partitioning operating system that is capable of responding to events from devices with an expected speed, as well as sharing processor time and memory between isolated partitions. A good example of such OS is the open-source POK (Partitioned Operating Kernel). In the repository, it contains an example design of a system for the quadcopters using AADL language for modeling its hardware and software. We apply such a technique with Model-driven engineering to a demo system that runs on real hardware and contains a flight management process with PID control as a partitioned process. Using a partitioned OS brings the reliability of flight system software to the next level. And to increase the level of control logic correctness we propose to use formal verification methods and provide examples of verifiable properties at the level of code using the deductive approach as well as at the level of the cyber-physical system using Differential dynamic logic to prove the stability.

1. Avionics application software standard interface, part 1 – required services, ARINC specification 653P1-3, November 15, 2010. Aeronautical radio, inc. (ARINC).

2. Delange J., Lec L. POK, an ARINC653-compliant operating system released under the BSD license. In Proc. of the 13th Real-Time Linux Workshop, 2011.

3. Delange J., Gilles O., Hugues J., and Pautet L. Model-Based Engineering for the Development of ARINC653 Architectures. SAE International Journal of Aerospace, vol. 3, no. 1, 2010, pp. 79-86.

4. Hugues J., Delange J. Model-based design and automated validation of ARINC653 architectures using the AADL. In Cyber-Physical System Design from an Architecture Analysis Viewpoint, Springer, 2017, pp. 33-52.

5. POK kernel repository. Available at: https://github.com/pok-kernel/pok.

6. Mallachiev K.M., Pakulin N.V., Khoroshilov A.V. Design and architecture of real-time operating system. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 2, 2016, pp. 181- 192. DOI: 10.15514/ISPRAS-2016-28(2)-12.

7. Солоделов Ю.А., Горелиц Н.К. Сертифицируемая бортовая операционная система реального времени JetOS для российских проектов воздушных судов. Труды ИСП РАН, том 29, вып. 3, 2017 г., стр. 171-178 / Solodelov Yu.A., Gorelits N.K. Certifiable onboard real-time operation system JetOS for Russian aircrafts design. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 3, 2017, pp. 171-178 (in Russian). DOI: 10.15514/ISPRAS-2017-29(3)-10.

8. JetOS. Available at: https://github.com/yoogx/forge.ispras.ru-git-chpok.

9. Khoroshilov A.V. On formalization of operating systems behaviour verification. In Proc. of the Eleventh International Conference on Computer Science and Information Technologies, Revised Selected Papers, 2017, pp. 168-172.

10. Кулямин В.В., Лаврищева Е.М., Мутилин В.С., Петренко А.К. Верификация и анализ вариабельных операционных систем. Труды ИСП РАН, том 28, вып. 3, 2016 г., стр. 189-208 / Kulyamin V.V., Lavrischeva E.M., Mutilin V.S., Petrenko A.K. Verification and analysis of variable operating systems, Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 3, 2016, pp. 189–208 178 (in Russian). DOI: 10.15514/ISPRAS-2016-28(3)-12

11. Khoroshilov A.V., Kuliamin V.V., Petrenko A.K. Verification of Operating System Components. System Informatics, No. 10, 2017, pp. 11-22.

12. Klein G. Operating system verification – An overview. Sadhana, vol. 34, no. 1, 2009, pp. 27-69

13. Giernacki W. et al. Crazyflie 2.0 quadrotor as a platform for research and education in robotics and control engineering. In Proc. of the 22nd International Conference on Methods and Models in Automation and Robotics (MMAR), 2017, pp. 37-42.

14. Crazyflie AADL Case Study. Available at: https://github.com/OpenAADL/Crazyflie.

15. Santoro C. How does a Quadrotor fly? A journey from physics. Available at: https://www.slideshare.net/corradosantoro/quadcopter-31045379.

16. Ardupulot project. Available at: http://ardupilot.org/copter.

17. Ardupulot project on Github. Available at: https://github.com/ArduPilot/ardupilot.

18. The CUAV Pixhack V3 flight controller board. Available at: https://docs.px4.io/en/flight_controller/pixhack_v3.html.

19. History of Ardupilot. Available at: http://ardupilot.org/planner2/docs/common-history-of-ardupilot.html.

20. Ardupilot. Advanced Tuning. Available at: http://ardupilot.org/copter/docs/tuning.html.

21. Copter Attitude Control. Available at: http://ardupilot.org/dev/docs/apmcopter-programming-attitude-control-2.html.

22. Hall Leonard. Practical PID implementation and the new Position Controller. ArduPilot UnConference, 2018. Available at: https://www.youtube.com/watch?v=-PC69jcMizA.

23. Park S., Deyst J., How J. A new nonlinear guidance logic for trajectory tracking. In Proc. of the AIAA guidance, navigation, and control conference and exhibit, 2004.

24. Delange J. AADL in Practice: Become an expert in software architecture modeling and analysis. Reblochon Development Company, 2017, 252 p.

25. POK. Examples. Case Study Ardupilot. Available at: https://github.com/pok-kernel/pok/tree/master/examples/case-study-ardupilot

26. Джозеф Ю. Ядро Cortex-M3 компании ARM. Полное руководство. Пер. с англ. АВ Евстифеева. Додэка-XXI, 2012, 552 стр. / Joseph Yiu. The Definitive Guide to the ARM Cortex-M3, 2nd Edition. Newnes, 2009, 479 p.

27. RaspberryPi-FreeRTOS. Demo. Drivers. Available at: https://github.com/jameswalmsley/RaspberryPi-FreeRTOS/tree/master/Demo/Drivers

28. Brandtstädter H. Sliding mode control of electromechanical systems. PhD Thesis, Technische Universität München, 2009.

29. Platzer A. Logical foundations of cyber-physical systems. Springer, 2018, 639 p.

30. Sergey Staroletov, Nikolay Shilov et al. Model-Driven Methods to Design of Reliable Multiagent Cyber-Physical Systems. In Proc. of the Conference on Modeling and Analysis of Complex Systems and Processes (MACSPro 2019), 2019.

31. Jan-David Quesel, Stefan Mitsch et al. How to model and prove hybrid systems with KeYmaera: a tutorial on safety. International Journal on Software Tools for Technology Transfer, vol. 18, №. 1, 2016, pp. 67-91.

32. Baar T., Staroletov S.M. A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier. Modeling and Analysis of Information Systems, vol. 25, №. 5, 2018, pp. 465-480.

33. Patrick Baudin, Jean-Christophe Filliâtre et al. ACSL: ANSI C Specification Language. Frama-C, 2008, 81 p.

34. Jochen Burghardt, Andreas Carben et al. ACSL by Example. DEVICE-SOFT project publication. Fraunhofer FIRST Institute, 2010, 134 p.