Modeling and Verification of A Timing Protection Mechanism in the OSEK/VDX OS using CSP

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.

This is a preview of subscription content, log in to check access.

References

  1. AG03

    DaimlerChrysler, A.G.: OSEK OS extensions for protected applications. Technical report, HIS (Hersteller Initiative Software) (2003)

    Google Scholar 

  2. AUT09

    GbR AUTOSAR (2009) Specification of operating system. V3, 1:R3

  3. BBFT06

    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

  4. BDT08

    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

  5. BFT09

    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

  6. CA11

    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

  7. Cho13

    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)

    Google Scholar 

  8. DMSW08

    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

  9. DRA04

    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

  10. ell18

    elliot (2018) A tool for transpiling C to go. https://github.com/elliotchance/c2go. Accessed 28 August 2019

  11. FFRJ12

    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)

  12. FM04

    Filliâtre, J.-C., Marché, C.: Multi-prover verification of c programs. International conference on formal engineering methods, pp. 15–29. Springer, Berlin (2004)

    Google Scholar 

  13. FZW+18

    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)

    Article  Google Scholar 

  14. G+01

    The OSEK Group (2001) OSEK/VDX time-triggered operating system specification, version 1.0

  15. GS88

    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)

    Article  Google Scholar 

  16. HDFT07

    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

  17. Hoa78

    Hoare, C.A.R.: Communicating sequential processes. Commun ACM 21(8), 666–677 (1978)

    Article  Google Scholar 

  18. HZZ+11

    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

  19. KEH+09

    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

  20. LRT92

    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

  21. LWZ+15

    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

  22. LZM04

    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

  23. PP16

    Prasertsang A, Pradubsuwun D (2016) Formal verification of concurrency in go. In: International joint conference on computer science and software engineering

  24. PQ08

    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)

    Google Scholar 

  25. RCGF97

    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)

    Article  Google Scholar 

  26. RS01

    Ryan, P., Schneider, S.A.: The modelling and analysis of security protocols: the CSP approach. Addison-Wesley Professional, Boston (2001)

    Google Scholar 

  27. SC04

    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

  28. SD05

    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

  29. SHZ+12

    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

  30. SLDP09

    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)

    Google Scholar 

  31. SZH+12

    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

  32. WDNSV07

    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

  33. WSSP07

    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)

    Google Scholar 

  34. XZW+16

    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

  35. YTW+14

    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)

    Article  Google Scholar 

  36. YZWW05

    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

  37. ZAC14

    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)

    Google Scholar 

  38. ZAL+13

    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

  39. Zhu13

    Zhu H (2013) Transformations between CSP and C. Ph.D

Download references

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

Affiliations

Authors

Corresponding author

Correspondence to Jianqi Shi.

Additional information

Publisher’s Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Jin Song Dong

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

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

Download citation

Keywords

  • Operating system
  • Modeling
  • Timing protection
  • Verification