Формальная модель партицированной операционной системы реального времени на Promela

Текущий стандарт надежного программного обеспечения для бортовых контроллеров – это многораздельная операционная система реального времени, которая способна реагировать на события от устройств с ожидаемой скоростью, а также делить процессорное время и память между изолированными разделами. Верификация на основе модели – это метод формальной проверки программного обеспечения, при котором разрабатывается программная модель, а затем она автоматически проверяется на соответствие формальным требованиям. Этот метод позволяет доказать правильность работы модели на всех возможных входных данных, всех возможных способов переключения процессов и взаимодействий. В этой статье описывается формализованная модель открытой многораздельной операционной системы POK, реализованная на языке Promela средства SPIN для формальной верификации методом Model Checking и предназначенная для моделирования поведения: планировщика разделов и процессов; системных вызовов через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательский код, осуществляющий работу нескольких процессов в разных разделах, которые синхронизируются через семафоры. Данный подход может быть использован для проверки корректности синхронизации, работы алгоритмов планировщика, корректного доступа к данным из разных разделов путем задания соответствующих требований в виде формул темпоральной логики линейного времени.

1. 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. Trudy ISP RAN/Proc. ISP RAS, vol. 31, issue 4, 2019. pp. 39-60. DOI: 10.15514/ISPRAS-2019-31(4)-3.

2. POK kernel repository. Available from: https://github.com/pok-kernel/pok, accessed 10.11.2020.

3. Basic Spin Manual. Available from: http://spinroot.com/spin/Man/Manual.html, accessed 10.11.2020.

4. Delange J. Intégration de la sécurité et de la sûreté de fonctionnement dans la construction d'intergiciels critiques. THÈSE, Télécom ParisTech, 2010 (in French).

5. 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, issue 1, 2009, pp. 79-86.

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

7. Specification ARINC. 653-2: Avionics application software standard interface: Part 1-required services. Technical report, Avionics Electronic Engineering Committee (ARINC), 2006.

8. Holzmann G. The model checker SPIN. In IEEE Transactions on software engineering, vol. 23, issue 5, 1997, pp. 279-295.

9. SPIN. Available from: https://github.com/nimble-code/Spin, accessed 10.11.2020.

10. Promela language reference. Available from: http://spinroot.com/spin/Man/promela.html, accessed 10.11.2020.

11. Старолетов С.М. Основы тестирования и верификации программного обеспечения. СПб., Лань, 2018 г., 344 стр. / Staroletov S. Basics of Verification and Testing. Spb., Lanbook, 2018, 344 p. (in Russuan).

12. Pnueli A. The temporal logic of programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46-57.

13. 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.

14. Khoroshilov A. On formalization of operating systems behaviour verification. In Proc. of the International Conference on Computer Science and Information Technology (CSIT), 2017, pp. 168-172.

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

16. Кулямин В.В., Лаврищева Е.М., Мутилин В.С., Петренко А.К. Верификация и анализ вариабельных операционных систем. Труды ИСП РАН, том 28, вып. 3, 2016 г., стр. 189-208 / Kuliamin 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 (in Russian). DOI: 10.15514/ISPRAS-2016-1(2)-12.

17. 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.

18. Солоделов Ю.А., Горелиц Н.К. Сертифицируемая бортовая операционная система реального времени JetOS для российских проектов воздушных судов. Труды ИСП РАН, том 29, вып. 3, 2017 г., стр. 171-178 / Solodelov Y. 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. DOI: 10.15514/ISPRAS-2017-29(3)-10.

19. Klein G. et al. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, 2009, pp. 207-220.

20. Staroletov S., Shilov N. Applying Model Checking Approach with Floating Point Arithmetic for Verification of Air Collision Avoidance Maneuver Hybrid Model. Lecture Notes in Computer Science, vol. 11636, 2019, pp. 193-207.

21. Staroletov S. Partitioned OS Model Implementation. Available at: https://github.com/SergeyStaroletov/PromelaSamples/blob/master/Sched.pml, accessed 10.11.2020. DOI: 10.5281/zenodo.3757397.

22. Старолетов С. Модель многораздельной операционной системы для целей формальной верификации. Государственная регистрация программы для ЭВМ, no. 2020614016, 2020 / Staroletov S. Partitioned OS model for formal verification purposes. State registration of computer software, no 2020614016, 2020 (in Russian).