首页> 外文期刊>Emerging Topics in Computing, IEEE Transactions on >Generation of Abstract Driver Models for IP Integration Verification
【24h】

Generation of Abstract Driver Models for IP Integration Verification

机译:生成IP集成验证的抽象驱动程序模型

获取原文
获取原文并翻译 | 示例

摘要

This paper proposes a new application of formal methods in the domain of low-level software (firmware) development of Embedded Systems. The development of low-level device drivers is difficult because of the complex interaction between the device hardware, the driver core routines and the application programmer's interface (API). Also the development of firmware components using such drivers is difficult because the driver specification may be ambiguous or erroneous or it may be misinterpreted by the developer. In this paper, we propose an abstract FSM model ("AFSM") to support systematic top-down development of low-level device drivers. The model serves as a formal specification that can be soundly refined into an implementation. The AFSM can also be generated semi-automatically in a bottom-up approach from the binary (machine code) of the driver. This allows for generating a formal documentation of a driver software that may be available as third-party IP for which no source code is available. The generated AFSM can serve as a technical reference during integration of such "black-box" driver IP and when developing firmware components that call the functions of the API. We present three case studies with industrial HW device and SW driver IPs demonstrating the potential of the proposed approach.
机译:本文提出了嵌入式系统低级软件(固件)开发领域正式方法的新应用。由于设备硬件,驱动程序核心例程与应用程序程序员接口(API)之间的复杂交互,低级设备驱动程序的开发很难。此外,使用这种驱动程序的固件组件的开发很难,因为驱动程序规范可能是模糊的或错误的,或者可能被开发人员误解。在本文中,我们提出了一种抽象的FSM模型(“AFSM”),以支持低级设备驱动程序的系统自上而下开发。该模型用作正式规范,可以完全精制到实现中。 AFSM也可以从驱动程序的二进制(机器代码)自动地生成半自动。这允许生成可以作为第三方IP可用的驱动程序软件的正式文档,其中没有源代码可用。生成的AFSM可以作为在这种“黑匣子”驱动程序IP的集成过程中作为技术参考,以及在调用API功能的固件组件时。我们展示了三种案例研究,工业HW设备和SW驱动器IPS展示了所提出的方法的潜力。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号