Preview

Труды Института системного программирования РАН

Расширенный поиск

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

https://doi.org/10.15514/ISPRAS-2019-31(4)-3

Полный текст:

Аннотация

Создание надежных беспилотных летательных аппаратов является важной задачей для науки и техники, потому что такие устройства могут иметь множество применений в современной жизни и в цифровой экономике, следовательно  необходимо обеспечивать надежность таких решений. В этой статье предлагается использование аппаратного прототипа квадрокоптера и разработка программного решения для полетного контроллера с высокими требованиями к надежности, которое будет соответствовать новым стандартам для программного обеспечения авионики и будет использовать существующие программные решения с открытым исходным кодом. В ходе исследования мы анализируем состав квадрокоптеров и полетных контроллеров для них. Мы описываем открытое программное обеспечение 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.


Для цитирования:


Старолетов С.М., Амосов М.С., Шульга К.М. Разработка программного обеспечения квадрокоптера с повышенными требованиями к надёжности на основе партицированной ОС и технологий формальной верификации. Труды Института системного программирования РАН. 2019;31(4):39-60. https://doi.org/10.15514/ISPRAS-2019-31(4)-3

For citation:


Staroletov S.M., Amosov M.S., Shulga K.M. Designing robust quadcopter software based on a real-time partitioned operating system and formal verification techniques. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(4):39-60. https://doi.org/10.15514/ISPRAS-2019-31(4)-3

Просмотров: 228


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)