Skip to main content
SpringerLink
Log in

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

  • Original Article
  • Published:
Formal Aspects of Computing

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 via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

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

    Google Scholar 

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

  3. 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. 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. 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. 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. 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)

    Chapter  Google Scholar 

  8. 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. 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. elliot (2018) A tool for transpiling C to go. https://github.com/elliotchance/c2go. Accessed 28 August 2019

  11. 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. 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. 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. The OSEK Group (2001) OSEK/VDX time-triggered operating system specification, version 1.0

  15. 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. 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. Hoare, C.A.R.: Communicating sequential processes. Commun ACM 21(8), 666–677 (1978)

    Article  Google Scholar 

  18. 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. 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. 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. 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. 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. Prasertsang A, Pradubsuwun D (2016) Formal verification of concurrency in go. In: International joint conference on computer science and software engineering

  24. 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)

    Chapter  Google Scholar 

  25. 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. Ryan, P., Schneider, S.A.: The modelling and analysis of security protocols: the CSP approach. Addison-Wesley Professional, Boston (2001)

    Google Scholar 

  27. 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. 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. 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. 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)

    Chapter  Google Scholar 

  31. 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. 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. 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)

    Chapter  Google Scholar 

  34. 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. 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. 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. 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. 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. 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

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, 3663 N. Zhongshan Rd., Shanghai, China

    Haiping Pang

  2. National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, 3663 N. Zhongshan Rd., Shanghai, China

    Yanhong Huang & Jianqi Shi

Authors
  1. Yanhong Huang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Haiping Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jianqi Shi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jianqi Shi.

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

Reprints and permissions

About this article

Check for updates. 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

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-020-00511-6

Keywords

Search

Navigation