Abstract
OSEK/VDX, a standard of automobile OS, was proposed to support the development of high-quality automotive applications. With its widely adopted, more and more automotive applications have been developed based on OSEK/VDX OS. As the continuously increasing complexity in the development of the applications, how to efficiently develop an application is becoming a challenge. A primary problem is the requirement specification may not be accurately and easily understood by the developers carrying out different tasks. The major reason is the usage of informal languages or notations in the specification. To solve this problem, formal specification provides a feasible solution. However, some difficulties (e.g., high requirement of significant abstraction and mathematical skills) has hindered the widely usage of formal methods. To address these difficulties, SOFL, a formal engineering methodology, has been proposed. In this paper, in order to investigate and study how SOFL can be used to help develop an OSEK/VDX application, we conduct a case study of cruise control system. Through the case study, we can see that SOFL specification can effectively help developer to develop an OSEK/VDX application throughout the development process.
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
OSEK/VDX Group. OSEK/VDX Operating System Specification 2.2.3. http://portal.osek-vdx.org/
Lemieux, J.: Programming in the OSEK/VDX Environment. CRC Press, Lawrence (2001)
Liu, S.: Formal engineering for industrial software development – an introduction to the sofl specification language and method. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 7–8. Springer, Heidelberg (2004)
Liu, S., Offutt, A.J., -Stuart, H., Sun, Y., Ohba, M.: SOFL: a formal engineering methodology for industrial applications. IEEE Trans. Softw. Eng. 24(1), 24–45 (1998)
Zhang, H., Aoki, T., Chiba, Y.: Yes! you can use your model checker to verify OSEK/VDX applications. In: Proceedings of the 8th IEEE International Conference on Software Testing, Verification and Validation, pp. 1–10, April 2015
Wang, X., Liu, S.: An approach to declaring data types for formal specifications. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 128–147. Springer, Heidelberg (2014)
H.-Stuart, C., Liu, S.: An operational semantics for SOFL. In: Proceedings of the Asia-Pacific Software Engineering Conference, pp. 52–61, December 1997
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 152(11), 74–84 (2009)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Yang, Z., Wang, C., Gupta, A.: Model checking sequential software programs via mixed symbolic analysis. CM Trans. Des. Autom. Electron. Syst. 14(1), 1–26 (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Cheng, Z., Zhang, H., Tan, Y., Lim, Y. (2016). A Case Study: SOFL + Model Checking for OSEK/VDX Application. In: Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2015. Lecture Notes in Computer Science(), vol 9559. Springer, Cham. https://doi.org/10.1007/978-3-319-31220-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-31220-0_10
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-31219-4
Online ISBN: 978-3-319-31220-0
eBook Packages: Computer ScienceComputer Science (R0)