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

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

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.