A Formal Model of a Partitioned Real-Time Operating System in Promela

Real-time partitioned operating systems meet the current avionics standard of reliable software; they are capable of responding to events from devices with an expected speed, as well as sharing processor time and memory between isolated partitions. Model-based Checking is a formal verification technique in which a software model is developed and then it is automatically checked for the compliance with formal requirements. This method allows proving the correct operation of the model on all possible input data, all possible ways of processes switching and interactions. In this article, we describe a formalized model of an open-source partitioned operating system POK. We implement the model in Promela language for SPIN tool with the purposes of formal verification using the Model Checking method. The model is designed to describe the behavior of: partition and process schedulers, system calls through a software interrupt, kernel libraries for working with synchronization primitives and processes awaiting, user code which consists of several processes in different partitions that are synchronized through a semaphore. The described approach can be used to verify the correct synchronization, the proper operation of the scheduler algorithms, and the accurate data access from different partitions by introducing the corresponding requirements in the form of formulas of the linear-time temporal logic.

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