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

点击翻译按钮获取中文摘要

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.