A case study: SOFL + model checking for OSEK/VDX application

OSEK/VDX, a standard of automobile OS, was proposed tosupport the development of high-quality automotive applications. Withits widely adopted, more and more automotive applications have beendeveloped based on OSEK/VDX OS. As the continuously increasingcomplexity in the development of the applications, how to efficientlydevelop an application is becoming a challenge. A primary problem isthe requirement specification may not be accurately and easily understoodby the developers carrying out different tasks. The major reason isthe usage of informal languages or notations in the specification. To solvethis problem, formal specification provides a feasible solution. However, some difficulties (e.g., high requirement of significant abstraction andmathematical 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 howSOFL can be used to help develop an OSEK/VDX application, we conducta case study of cruise control system. Through the case study, wecan see that SOFL specification can effectively help developer to developan OSEK/VDX application throughout the development process.5th International Workshop, SOFL+MSVL 2015, Paris, France, November 6, 2015. Revised Selected Paper