• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Asia-Pacific Software Engineering Conference >Modeling OSEK/VDX OS Requirements in C
【24h】

Modeling OSEK/VDX OS Requirements in C

机译：在C中建模OSEK / VDX OS需求

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper presents an approach to use C language to model underlying operating systems widely used in the domain of automotive control software. The greatest benefit of using C, a programming language, which is used widely in this domain, is the elimination of the heterogeneity between OS model and control software. This enables us to formally verify control software while keeping its own characteristics such as function calls, the use of external libraries, and dynamic memory allocation. We took a two-step approach to maintain the level of abstraction; we first define formal CSP models of OS components based on the OSEK/VDX international standard and then define an OS model in C by using the CSP models as references. We derived 20 functional API assertions, 6 invariant properties, 4 temporal properties and 4 code-safety properties from the OSEK/VDX international standard, and validated the model with the C code model checker CBMC. We used our OS C model to verify applications for Erika OS and could find out severe property violations.
机译：本文提出了一种使用C语言对汽车控制软件领域中广泛使用的底层操作系统进行建模的方法。使用C（一种在该领域广泛使用的编程语言）的最大好处是消除了OS模型与控制软件之间的异质性。这使我们能够正式验证控制软件，同时保留其自身的特性，例如函数调用，外部库的使用和动态内存分配。我们采取了两步方法来保持抽象水平。我们首先基于OSEK / VDX国际标准定义OS组件的正式CSP模型，然后通过使用CSP模型作为参考在C中定义OS模型。我们从OSEK / VDX国际标准派生了20个功能API断言，6个不变属性，4个时间属性和4个代码安全属性，并使用C代码模型检查器CBMC验证了该模型。我们使用OS C模型来验证Erika OS的应用程序，并可以发现严重的属性违规情况。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号