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

构建高能效和高性能的嵌入式系统需要硬件/软件(硬件/软件)的协同设计，因此需要协同验证。嵌入式系统日益增长的复杂性产生了对可扩展协同验证的迫切需求。本项目的中心目标是开发一种基于组件的嵌入式系统软硬件协同验证的统一方法，该方法将模型检测有效地集成到基于组件的嵌入式系统开发中，并利用基于组件的系统架构进行可扩展的协同验证。该方法的核心是三个创新概念的协同集成：(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.