Разработка программного обеспечения квадрокоптера с повышенными требованиями к надёжности на основе партицированной ОС и технологий формальной верификации

Создание надежных беспилотных летательных аппаратов является важной задачей для науки и техники, потому что такие устройства могут иметь множество применений в современной жизни и в цифровой экономике, следовательно  необходимо обеспечивать надежность таких решений. В этой статье предлагается использование аппаратного прототипа квадрокоптера и разработка программного решения для полетного контроллера с высокими требованиями к надежности, которое будет соответствовать новым стандартам для программного обеспечения авионики и будет использовать существующие программные решения с открытым исходным кодом. В ходе исследования мы анализируем состав квадрокоптеров и полетных контроллеров для них. Мы описываем открытое программное обеспечение Ardupilot для беспилотных летательных аппаратов, контроллер APM и методы ПИД-регулирования. Сегодняшним стандартом надежного программного обеспечения для бортовых контроллеров являются партицированные операционные системы реального времени, которые способны реагировать на события от оборудования с ожидаемой скоростью, а также разделять процессорное время и память между изолированными разделами. Хорошим примером такой ОС с открытым исходным кодом является POK (Partitioned Operating Kernel). В репозитории она содержит пример описания системы для дронов с использованием языка AADL с моделированием аппаратного и программного обеспечения решения. Мы применяем такую технику к демонстрационной системе, которая работает на реальном оборудовании и содержит процесс управления полетом с PID-регулятором в виде изолированного процесса. Использование партицированной ОС выводит надежность программного обеспечения полетного контроллера на новый уровень. Для того, чтобы повысить уровень корректности логики управления, мы предлагаем использовать формальные методы верификации и демонстрируем примеры проверяемых свойств на уровне кода, используя дедуктивный подход, а также проводя моделирование на уровне киберфизической системы с использованием динамической дифференциальной логики для доказательства устойчивости.

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.