CSR: SHF: Small: Automata-Theorectic Approach to Hardware/Software Co-Verification

CSR：SHF：小型：硬件/软件协同验证的自动机理论方法

• 批准号: 0916968
• 负责人: Fei Xie
• 金额: $ 40.21万
• 依托单位: Portland State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2013-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0916968&HistoricalAwards=false
• 关键词: CSR; SHF; Small; Automata; Theorectic

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).Computer systems such as personal computers and embedded systems are increasingly pervasive. People's everyday lives depend on these systems. Therefore, they must be high-confidence. To boost system performance, hardware and software are often closely coupled for optimizations. As a result, separate verification of software and hardware cannot guarantee the correctness of the entire system; thus hardware/software (HW/SW) co-verification, verifying the hardware and software together, is highly desired. There are four major benefits from co-verification: (1) advocating design-level HW/SW interface specifications, (2) facilitating early hardware and software verification in the system context, (3) reducing verification complexity by properly leveraging HW/SW couplings, and (4) broadening property coverage to the entire system. This project develops an automata-theoretic approach to HW/SW co-verification. Major research tasks include: (1) developing a co-specification scheme for hardware and software, (2) developing an automata-theoretic model for co-verification and its model checking algorithms, (3) developing abstraction/refinement algorithms for co-verification, (4) developing a co-verification toolkit supporting this approach, and (5) evaluating this approach and the toolkit on device-driver co-verification. Education and outreach efforts include (1) collaborating with industrial partners on device-driver co-verification, (2) creating video demonstration of this research and make it available online for education and research purposes, (3) integrating research activities and results of this project into a three course software engineering sequence, (4) advising and mentor undergraduate and graduate students to conduct research in this project, and (5) broadening participation through outreach efforts.

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。计算机系统，如个人电脑和嵌入式系统越来越普遍。人们的日常生活依赖于这些系统。因此，他们必须高度自信。为了提高系统性能，硬件和软件通常紧密耦合以进行优化。因此，软件和硬件的单独验证不能保证整个系统的正确性;因此，高度期望硬件/软件（HW/SW）协同验证，即一起验证硬件和软件。协同验证有四个主要好处：（1）倡导设计级硬件/软件接口规范，（2）促进系统环境中的早期硬件和软件验证，（3）通过适当利用硬件/软件耦合降低验证复杂性，以及（4）将属性覆盖范围扩大到整个系统。本计画发展一种自动机理论的软硬件协同验证方法。主要研究任务包括：（1）开发软硬件协同规范设计方案;（2）开发协同验证的自动机理论模型及其模型检测算法;（3）开发协同验证的抽象/精化算法;（4）开发支持该方法的协同验证工具包;（5）评估该方法和工具包在设备驱动协同验证中的应用。教育和推广工作包括（1）与工业合作伙伴合作进行设备驱动程序协同验证，（2）创建本研究的视频演示，并将其在线提供用于教育和研究目的，（3）将本项目的研究活动和结果整合到三门课程的软件工程序列中，（4）建议和指导本科生和研究生在本项目中进行研究，以及（5）通过外联工作扩大参与。