A case study: SOFL + model checking for OSEK/VDX application
A case study: SOFL + model checking for OSEK/VDX application
复制标题
案例研究：OSEK/VDX 应用的 SOFL 模型检查
DOI：
10.1007/978-3-319-31220-0_10
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Yasuo TAN and Yuto LIM
中科院分区：
文献类型：
--
作者：
Zhuo CHENG;Haitao ZHANG;Yasuo TAN and Yuto LIM
OSEK/VDX是一种汽车操作系统标准，旨在支持高质量的汽车应用程序的开发。随着OSEK/VDX操作系统的广泛应用，越来越多的汽车应用程序基于OSEK/VDX操作系统进行开发。随着应用程序开发的复杂性不断增加，如何高效地开发应用程序成为一个挑战。一个主要的问题是需求规范可能不准确，容易被执行不同任务的开发人员理解。主要原因是在规范中使用了非正式的语言或符号。为解决这一问题，形式化规约提供了一种可行的解决方案.然而，一些困难（例如，对抽象和数学技能的高要求）阻碍了形式化方法的广泛应用。为了解决这些困难，SOFL，一个正式的工程方法，已被提出。在本文中，为了调查和研究如何SOFL可以用来帮助开发一个OSEK/VDX应用程序，我们进行了巡航控制系统的案例研究。通过案例研究，我们可以看到SOFL规范可以有效地帮助开发人员在整个开发过程中开发OSEK/VDX应用程序。
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.