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 and event synchronization 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Abdeddaïm, Y., Maler, O.: Preemptive job-shop scheduling using stopwatch automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_9
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9_7
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). https://doi.org/10.1007/BFb0020949
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27755-2_3
Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16
Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7
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). https://doi.org/10.1109/CoDIT.2018.8394813
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16
Deifel, H.P., Göttlinger, M., Milius, S., Schröder, L., Dietrich, C., Lohmann, D.: Automatic verification of application-tailored OSEK kernels. In: IEEE (2017)
EV3RT Project: EV3RT (2019). https://ev3rt-git.github.io/about/
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)
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 2008, pp. 131–136. ACM (2008). https://doi.org/10.1145/1450135.1450166
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 (2011)
Klein, G., et al.: sel4: formal verification of an OS kernel. In: ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009. ACM (2009). https://doi.org/10.1145/1629575.1629596
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 (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), 1–25 (017). https://doi.org/10.1145/3015777
TOPPERS Project: Toyohashi open platform for embedded real-time systems. https://www.toppers.jp/en/project.html
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 02 Sep 2021
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 (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., Chiba, Y.: Verifying OSEK/VDX applications: a sequentialization-based model checking approach. IEICE Trans. Inf. Sys. 98(10), 1765–1776 (2015)
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 (2013)
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)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Adelt, J., Gebker, J., Herber, P. (2022). Towards Reusable Formal Models for Custom Real-Time Operating Systems. In: Groote, J.F., Huisman, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2022. Lecture Notes in Computer Science, vol 13487. Springer, Cham. https://doi.org/10.1007/978-3-031-15008-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-031-15008-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-15007-4
Online ISBN: 978-3-031-15008-1
eBook Packages: Computer ScienceComputer Science (R0)