Abstract
In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling, event synchronization, and communication abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior, together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
TRON\(.\mu \)ITRON4.0 specification (2007). https://www.tron.org/wp-content/themes/dp-magjam/pdf/specifications/en_US/TEF024-S001-04.03.00_en.pdf. Accessed: 2021-09-02
Abdeddaim, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 113–126. Springer, Berlin (2002)
Adelt, J., Gebker, J., Herber, P.: Towards reusable formal models for custom real-time operating systems. In: Formal Methods for Industrial Critical Systems: 27th International Conference, FMICS 2022, Warsaw, Poland, September 14–15, 2022, Proceedings. pp. 14–15. Springer, Berlin (2022)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Bechennec, J.-L., Briday, M., Faucou, S., Trinquet, Y.: Trampoline an open source implementation of the OSEK/VDX RTOS specification. In: 2006 IEEE Conference on Emerging Technologies and Factory Automation, pp. 62–69. IEEE, New York (2006)
Béchennec, J.-L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In: 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT), pp. 628–634 (2018)
Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal pp. 200–236. Springer, Berlin (2004)
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lecture Notes on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Berlin (2004)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal — a tool suite for automatic verification of real-time systems. In: Workshop on Verification and Control of Hybrid Systems. LNCS, vol. 1066, pp. 232–243. Springer, Berlin (1995)
Beyer, D., Keremoglu, M.E.: CPACHECKER: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, pp. 184–190. Springer, Berlin (2011)
Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) Integrated Formal Methods, pp. 102–110. Springer, Cham (2017)
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: International Conference on Software Engineering and Formal Methods, pp. 233–247. Springer, Berlin (2012)
Deifel, H.-P., Göttlinger, M., Milius, S., Schröder, L., Dietrich, C., Lohmann, D.: Automatic verification of application-tailored OSEK kernels. In: Formal Methods in Computer Aided Design (FMCAD), Vienna, Austria. IEEE, New York (2017)
EV3RT Project. EV3RT (2019). https://ev3rt-git.github.io/about/
Gu, R., Shao, Z., Chen, H., Newman Wu, X., Kim, J., Sjöberg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pp. 653–669 (2016)
Han, P., Zhai, Z., Nielsen, B., Nyman, U.: Model-based optimization of ARINC-653 partition scheduling. Int. J. Softw. Tools Technol. Transf. 23(5), 721–740 (2021)
Haur, I., Béchennec, J.-L., Roux, O.H.: Formal schedulability analysis based on multi-core RTOS model. In: 29th International Conference on Real-Time Networks and Systems, pp. 216–225 (2021)
Haur, I., Béchennec, J.-L., Roux, O.H.: Formal verification of the inter-core synchronization of a multi-core RTOS kernel. In: International Conference on Formal Engineering Methods, pp. 140–155. Springer, Berlin (2022)
Herber, P., Fellmuth, J., Glesner, S.: Model checking SystemC designs using timed automata. In: IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS’08, Atlanta, GA, USA. pp. 131–136. ACM, New York (2008)
Huang, Y., Zhao, Y., Zhu, L., Li, Q., Zhu, H., Shi, J.: Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: 2011 Fifth International Conference on Theoretical Aspects of Software Engineering, pp. 142–149. IEEE, New York (2011)
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: SeL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP’09, Montana, USA, pp. 207–220. ACM, New York (2009)
Laplante, P.A., et al.: Real-Time Systems Design and Analysis. Wiley, New York (2004)
OSEK. ISO 17356-3:2005 Road vehicles — open interface for embedded automotive applications — part 3: OSEK/VDX operating system (OS). International Organization for Standardization (2005)
Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: formal verified OSEK/VDX real-time operating system. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, pp. 293–301. IEEE, New York (2012)
Tigori, K.T.G., Béchennec, J.-L., Faucou, S., Roux, O.H.: Formal model-based synthesis of application-specific static RTOS. ACM Trans. Embed. Comput. Syst. 16(4) (2017)
TOPPERS Project. Toyohashi open platform for embedded real-time systems. https://www.toppers.jp/en/project.html
Vu, D.H., Chiba, Y., Yatake, K., Aoki, T.: Verifying OSEK/VDX OS design using its formal specification. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 81–88. IEEE, New York (2016)
Waszniowski, L., Hanzálek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Syst. 38(1), 39–65 (2008)
Zhang, H., Aoki, T., Lin, H.-H., Zhang, M., Chiba, Y., Yatake, K.: SMT-based bounded model checking for OSEK/VDX applications. In: 2013 20th Asia-Pacific Software Engineering Conference (APSEC), vol. 1, pp. 307–314. IEEE, New York (2013)
Zhang, H., Aoki, T., Chiba, Y.: Verifying OSEK/VDX applications: a sequentialization-based model checking approach. IEICE Trans. Inf. Syst. 98(10), 1765–1776 (2015)
Zhang, H., Li, G., Cheng, Z., Xue, J.: Verifying OSEK/VDX automotive applications: a spin-based model checking approach. Softw. Test. Verif. Reliab. 28(3), e1662 (2018)
Funding
Open Access funding enabled and organized by Projekt DEAL.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Adelt, J., Gebker, J. & Herber, P. Reusable formal models for concurrency and communication in custom real-time operating systems. Int J Softw Tools Technol Transfer 26, 229–245 (2024). https://doi.org/10.1007/s10009-024-00743-4
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-024-00743-4