Abstract
Checking compliance of a Real-Time Operating System (RTOS) with the standard it is supposed to implement is usually achieved by executing a test suite. That is, for example, the case for OS conforming to the AUTOSAR standard. The task becomes complex for multi-core implementations because simultaneous executions are usually not tested and are, in any case, difficult to test generically as the possible interleaving depends on the execution speeds of the cores. In this paper, we propose to use model-checking to verify the communication and synchronization mechanisms involved in the concurrent execution of OS services: concurrent accesses to OS data structures, multi-core scheduling, and inter-core interrupt handling. The multi-core operating system and the application are modeled by a High-level Colored Time Petri Nets (HCTPN) reproducing the control flow graph and using the same variables as the actual implementation. This approach allows to verify compliance with some standards. This paper focuses on rare situations with simultaneous service calls in parallel on several cores that are almost impossible to test on real implementation but that we will be able to obtain by our model checking method. We applied our approach to an OSEK and AUTOSAR compliant RTOS called Trampoline.
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
Notes
- 1.
The two double dot ( : : ) are equivalent to an arc in the model. This syntax proposed by Roméo allows a clear and better organization of the Petri subnet in different XML files, which form only one Petri net. Thus a function call is ensured by the following syntax: the XML file name of the Petri subnet:: the place name to which we want to send a token.
References
AUTOSAR GbR: Specification of operating system (2009)
Béchennec, J.L., Briday, M., Faucou, S., Trinquet, Y.: Trampoline an open source implementation of the OSEK/VDX RTOS specification. In: IEEE Conference on Emerging Technologies and Factory Automation, ETFA 2006, pp. 62–69 (2006)
Béchennec, J.L., Roux, O.H., Tigori, T.: Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In: International Conference on Control, Decision and Information Technologies (CODIT 2018). IEEE (2018)
Boyer, M., Diaz, M.: Multiple enabledness of transitions in petri nets with time. In: 9th International Workshop on Petri Nets and Performance Models, PNPM 2001, pp. 219–228. IEEE Computer Society (2001)
Choi, Y.: Safety analysis of trampoline OS using model checking: an experience report. In: 2011 IEEE 22nd International Symposium on Software Reliability Engineering, pp. 200–209 (2011)
Espinosa, T., Leon, G.: Formal verification of a real-time operating system. Master thesis, University of Saskatchewan (2012)
Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker, pp. 888–891. Association for Computing Machinery, New York (2018)
Gu, R., et al.: Building certified concurrent OS kernels. Commun. ACM 62(10), 89–99 (2019)
Haur, I., Béchennec, J.L., Roux, O.H.: High-level colored time petri nets for true concurrency modeling in real-time software. In: International Conference on Control, Decision and Information Technologies (CODIT 2022). IEEE (2022)
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, RTNS 2021, pp. 216–225 (2021)
Hillah, L., Kordon, F., Petrucci, L., Trèves, N.: PN standardisation: a survey. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 307–322. Springer, Heidelberg (2006). https://doi.org/10.1007/11888116_23
ISO: ISO 26262:2018 road vehicles – functional safety. Technical report, ISO (2018)
Klein, G., et al.: Sel4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, New York, NY, USA, pp. 207–220 (2009)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE–3(2), 125–143 (1977)
Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54–57. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_6
OSEK Group: OSEK/VDX OS test plan version 2.0 (1999)
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. (TECS) 16(4), 1–25 (2017)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Haur, I., Béchennec, JL., Roux, O.H. (2022). Formal Verification of the Inter-core Synchronization of a Multi-core RTOS Kernel. In: Riesco, A., Zhang, M. (eds) Formal Methods and Software Engineering. ICFEM 2022. Lecture Notes in Computer Science, vol 13478. Springer, Cham. https://doi.org/10.1007/978-3-031-17244-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-17244-1_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17243-4
Online ISBN: 978-3-031-17244-1
eBook Packages: Computer ScienceComputer Science (R0)