CSR---EHS: Component-Based Hardware/Software Co-Verification of Embedded Systems

构建高能效和高性能的嵌入式系统需要硬件/软件（HW/SW）协同设计，因此需要协同验证。嵌入式系统的复杂性不断增加，迫切需要可扩展的协同验证。该项目的中心目标是开发一种基于组件的嵌入式系统软硬件协同验证的统一方法，该方法有效地将模型检测集成到基于组件的嵌入式系统开发中，并利用基于组件的系统架构进行可扩展的协同验证。该方法的核心是三个创新概念的协同集成：（1）统一的属性规范语言，它支持硬件和软件的统一和一致的属性规范，从而实现跨硬件/软件语义边界的组合推理;（2）统一的组件模型，它为硬件和软件组件提供统一的表示，从而实现基于组件的抽象和精化;以及（3）平台概念，它捕获特定领域的知识，特别是体系结构模式，它为系统和组件属性的自动公式化和分解提供支持。这种集成有可能大大推进最先进的可扩展的协同验证的嵌入式系统的基础上，有效地利用基于组件的架构和系统重用的验证工作。该项目通过两个不同的渠道产生广泛的影响：（1）向工业合作伙伴转让技术;（2）通过向本科生和研究生提供课程进行传播。除了通过讲座和科学博览会招募少数民族和妇女的传统外联工作外，还为参加该项目的学生提供实习机会。

Building power-efficient and high-performance embedded systems demands hardware/software (HW/SW) co-design and, therefore, co-verification. The growing complexity of embedded systems generates an acute need for scalable co-verification. The central objective of this project is to develop a unified approach to component-based HW/SW co-verification of embedded systems, which effectively integrates model checking into component-based development of embedded systems and leverages component-based system architectures for scalable co-verification. The core of this approach is the synergistic integration of three innovative concepts: (1) a unified property specification language that supports uniform and coherent property specification for hardware and software, thus enabling compositional reasoning across the HW/SW semantic boundary; (2) a unified component model that provides a uniform representation for hardware and software components, thus enabling component-based abstraction and refinement; and (3) a platform concept that captures domain-specific knowledge, in particular, architectural patterns, which provides support for automatic formulation and decomposition of system and component properties. This integration has potential for substantially advancing the state of the art in scalable co-verification of embedded systems based on effective leverage of component-based architectures and systematic reuse of verification effort. This project has broad impact through two separate venues: (1) technology transfer to industrial partners and (2) dissemination through course delivery to undergraduate and graduate students. In addition to traditional outreach efforts to recruit minorities and women through lectures and science fairs, opportunities for internships are provided to students participating in this project.