Abstract
The functions of automobiles are becoming increasingly intelligent, which leads to the increasing number of electrical control units for one automobile. Hence, it makes software migration and extension more complicated. In order to avoid these problems, the standard OSEK/VDX has been proposed jointly by a German automotive company consortium and the University of Karlsruhe. This standard provides specifications for the development of automotive software, this standard has become one of the major standards for real-time automotive operating systems (OSs). Since errors in the automotive OS may pose threat to the safety of people in a vehicle, it is necessary to verify the correctness of the OSEK OS which is used by many manufacturers around the world. Formal methods can be adopted to verify the correctness of both software and hardware. Therefore, we propose a formal model of the OSEK OS at the code level and verify three significant properties of the OSEK-based system. In this study, the code-level OSEK OS is verified to ensure compliance with the specifications. An automotive OS always requires that the systemreacts in a timelymanner to external events and performs the computations within the timing constraints. However, there is a possibility that the running time of the tasks exceeds the timing requirements due to the complexity of the tasks. Therefore, by referring to one of the extensions of the OSEK OS, Automotive Open System Architecture (AUTOSAR), we proposed tpOSEK, which is capable of extending the OSEK OS with a timing protection mechanism in AUTOSAR in this study. In our previous study, it was verified that the higher-priority task cannot be preempted by lower-priority tasks. In this paper, after improvement made to the OSEK OS model by adding interrupt service routine models and alarms, and extension of the OSEK OS model with a timing protection model, we have verified that tpOSEK satisfies three significant properties, which include deadlock f ree, complete and no timeout. These properties represent the basic conditions for the systemto run smoothly. If such properties as deadlock f ree and complete are satisfied, it means no deadlock is encountered by this system and all of the tasks can be scheduled completely. Moreover, if the property timeout cannot be satisfied, it means that none of the tasks would miss the deadline. Based on the tpOSEK model, the correct timing protection APIs can be designed at the code level. Thus, by extending the OSEKOSwith theseAPIs,we can update theOSEKOS faster and the need tomodify the dependent applications can be removed. Furthermore, we have constructed formal models for two industrial cases based on tpOSEK OS to demonstrate the soundness of our methods.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
DaimlerChrysler, A.G.: OSEK OS extensions for protected applications. Technical report, HIS (Hersteller Initiative Software) (2003)
GbR AUTOSAR (2009) Specification of operating system. V3, 1:R3
Bechennec J-L, Briday M, Faucou S, Trinquet Y (2006) Trampoline an open source implementation of the OSEK/VDX RTOS specification. In: IEEE Conference on emerging technologies and factory automation (ETFA 2006). IEEE, pp 62–69
Brun M, Delatour J, Trinquet Y (2008) Code generation from aadl to a real-time operating system: an experimentation feedback on the use of model transformation. In: IEEE Conference on engineering of complex computer systems (ICECCS 2008). IEEE, pp 257–262
Bertrand D, Faucou S, Trinquet Y (2009) An analysis of the autosar os timing protection mechanism. In: IEEE Conference on emerging technologies and factory automation (ETFA 2009). IEEE, pp 1–8
Chen J, Aoki T (2011) Conformance testing for OSEK/VDX operating system using model checking. In: Asia-Pacific software engineering conference (APSEC 2011). IEEE, pp 274–281
Choi, Y.: Constraint specification and test generation for osek/vdx-based operating systems. International conference on software engineering and formal methods, pp. 305–319. Springer, Berlin (2013)
Diederichs C, Margull U, Slomka F, Wirrer G (2008) An application-based EDF scheduler for OSEK/VDX. In: Proceedings of the conference on design, automation and test in Europe. ACM, pp 1045–1050
De Renesse F, Aghvami AH (2004) Formal verification of ad-hoc routing protocols using spin model checker. In: Proceedings of the 12th IEEE Mediterranean electrotechnical conference (MELECON 2004), vol 3. IEEE, pp 1177–1182
elliot (2018) A tool for transpiling C to go. https://github.com/elliotchance/c2go. Accessed 28 August 2019
Ficek C, Feiertag N, Richter K, Jersak M (2012) Applying the autosar timing protection to build safe and efficient iso 26262 mixed-criticality systems. Embedded real time software and systems (ERTS)
Filliâtre, J.-C., Marché, C.: Multi-prover verification of c programs. International conference on formal engineering methods, pp. 15–29. Springer, Berlin (2004)
Fei, Y., Zhu, H., Wu, X., Fang, H., Qin, S.: Comparative modelling and verification of pthreads and dthreads. J Softw Evol Process 30(3), e1919 (2018)
The OSEK Group (2001) OSEK/VDX time-triggered operating system specification, version 1.0
Goodenough, J.B., Sha, L.: The priority ceiling protocol: a method for minimizing the blocking of high priority Ada tasks. ACM SIGAda Ada Lett VII I(7), 20–31 (1988)
Hladik P-E, Déplanche A-M, Faucou S, Trinquet Y (2007) Adequacy between AUTOSAR OS specification and real-time scheduling theory. In: International symposium on industrial embedded systems (SIES 2007). IEEE, pp 225–233
Hoare, C.A.R.: Communicating sequential processes. Commun ACM 21(8), 666–677 (1978)
Huang Y, Zhao Y, Zhu L, Li Q, Zhu H, Shi J (2011) Modeling and verifying the code-level OSEK/VDX operating system with CSP. In: Fifth international symposium on theoretical aspects of software engineering (TASE 2011). IEEE, pp 142–149
Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M et al (2009) seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on operating systems principles. ACM, pp 207–220
Lehoczky JP, Ramos-Thuel S (1992) An optimal algorithm for scheduling soft-aperiodic tasks in fixed-priority preemptive systems. In: Real-time systems symposium, 1992. IEEE, pp 110–123
Li B, Wang M, Zhao Y, Pu G, Zhu H, Song F (2015) Modeling and verifying Google file system. In: IEEE 16th International symposium on high assurance systems engineering (HASE 2015). IEEE, pp 207–214
Lei W, Zhaohui W, Mingde Z (2004) Worst-case response time analysis for OSEK/VDX compliant real-time distributed control systems. In: Proceedings of the 28th annual international on computer software and applications conference (COMPSAC 2004). IEEE, pp 148–153
Prasertsang A, Pradubsuwun D (2016) Formal verification of concurrency in go. In: International joint conference on computer science and software engineering
Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). International joint conference on automated reasoning, pp. 171–178. Springer, Berlin (2008)
Ripoll, I., Crespo, A., García-Fornes, A.: An optimal algorithm for scheduling soft aperiodic tasks in dynamic-priority preemptive systems. IEEE Trans Softw Eng 23(6), 388–400 (1997)
Ryan, P., Schneider, S.A.: The modelling and analysis of security protocols: the CSP approach. Addison-Wesley Professional, Boston (2001)
Scaife N, Caspi P (2004) Integrating model-based design and preemptive scheduling in mixed time-and event-triggered systems. In: 16th Euromicro conference on real-time systems (ECRTS 2004). IEEE, pp 119–126
Schneider S, Delicata R (2005) Verifying security protocols: an application of CSP. In: Communicating sequential processes. The first 25 years. Springer, Berlin, pp 243–263
Shi J, He J, Zhu H, Fang H, Huang Y, Zhang X (2012) ORIENTAIS: formal verified OSEK/VDX real-time operating system. In: 17th International conference on engineering of complex computer systems (ICECCS 2012). IEEE, pp 293–301
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. International conference on computer aided verification, pp. 709–714. Springer, Berlin (2009)
Shi J, Zhu L, Huang Y, Guo J, Zhu H, Fang H, Ye X (2012) Binary code level verification for interrupt safety properties of real-time operating system. In: 2012 Sixth international symposium on theoretical aspects of software engineering (TASE). IEEE, pp 223–226
Wang G, Di Natale M, Sangiovanni-Vincentelli A (2007) An OSEK/VDX implementation of synchronous reactive semantics preserving communication protocols. In: Workshop on operating systems platforms for embedded real-time applications, p 38
Wawersich, C., Stilkerich, M., Schröder-Preikschat, W.: An OSEK/VDX-based multi-JVM for automotive appliances. Embedded system design: topics, techniques and trends, pp. 85–96. Springer, Berlin (2007)
Xie W, Zhu H, Wu X, Xiang S, Guo J (2016) Modeling and verifying HDFS using CSP. In: IEEE 40th annual on computer software and applications conference (COMPSAC 2016), vol 1. IEEE, pp 221–226
Yuan, T., Tang, Y., Wu, X., Zhang, Y., Zhu, H., Guo, J., Qin, W.: Formalization and verification of REST on HTTP using CSP. Electron Notes Theor Comput Sci 309, 75–93 (2014)
Yang G, Zhao M, Wang L, Wu Z (2005) Model-based design and verification of automotive electronics compliant with OSEK/VDX. In: Second international conference on embedded software and systems, 2005. IEEE, p 7
Zhang, H., Aoki, T., Chiba, Y.: A spin-based approach for checking OSEK/VDX applications. International workshop on formal techniques for safety-critical systems, pp. 239–255. Springer, Berlin (2014)
Zhang H, Aoki T, Lin H-H, Zhang M, Chiba Y, Yatake K (2013) SMT-based bounded model checking for OSEK/VDX applications. In: 20th Asia-Pacific software engineering conference (APSEC 2013), vol 1. IEEE, pp 307–314
Zhu H (2013) Transformations between CSP and C. Ph.D
Acknowledgements
Funding was provided byNational Natural Science Foundation of China (Grant No. 61602178) and Science and Technology Commission of Shanghai Municipality (Grant No. 18QB1402000).
Author information
Authors and Affiliations
Corresponding author
Additional information
Jin Song Dong
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Huang, Y., Pang, H. & Shi, J. Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP. Form Asp Comp 32, 113–145 (2020). https://doi.org/10.1007/s00165-020-00511-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-020-00511-6