基于高阶规约定向测试的异构系统验证研究

Since last decade, we have witnessed the continuously rapid development in embedded system domain. More and more state-of-the-art embedded systems adopt the heterogeneous multi-processor platform rather than the platform with single core. At the meanwhile, to achieve better quality and performance, the design paradigm shift from simple control system to complex heterogeneous Cyber-Physical Systems （CPS） is gaining more interests. Increasing complexity coupled with time-to-market pressure create a critical need to validate heterogeneous embedded system designs. The functional validation is thus widely acknowledged as a major bottleneck in embedded system design. To guarantee the reliability of heterogeneous embedded systems, up to 70% of the overall design time and resources are spent on functional validation...The objective of this project is to reduce the overall validation efforts in the top-down design flow of heterogeneous system design using the high-level specifications. In this project, we are going to address the following three major problems: i) Formal modeling of high-level specifications. This project will investigate how to modeling the heterogeneous system with multiple model of computation (MoC) and how to extract the formal models from system-level specifications to enable automated analysis. ii) Efficient validation of system-level specifications with minimum effort. This project will investigate the automated directed test generation for high-level specification validation. We will explore various approaches and techniques to further reduce the directed test generation time. iii) Consistency checking between different abstraction layers. This project will explore the possibility of reusing high-level validation efforts for low-level implementation validation as well as to check the consistency between different abstraction layers...In conclusion, this project targets to improve the effectiveness and efficiency of functional validation of heterogeneous embedded systems. We believe that our approaches can not only enhance the reliability of heterogeneous embedded systems, but also reduce the time-to-market.

随着体系结构从单核模式到异构多核模式，处理对象从简单控制系统到异构信息物理融合系统的渐进演化，嵌入式系设计的复杂性越来越高。大量的时间与资源被消耗在系统功能验证上，在时间与效率方面功能验证已经成为了系统设计的主要瓶颈。本项目将基于系统设计高阶规约，研究如何提高自顶向下设计流程各个测试验证环节的效率，有效降低异构系统验证的复杂性。研究内容主要包括：1)研究异构系统高阶规约的形式化建模与模型自动抽取方法，提高对系统基本功能特征的描述与自动化分析能力；2)研究基于高阶规约的自动化测试用例生成的优化方法，提高异构系统设计与开发的效率；3)研究如何提高异构系统自顶向下设计过程中各阶段验证结果的重用技术，确保系统从系统高阶规约到具体实现逐步精化过程中的一致性与正确性。从而提高系统的整体验证效率。在缩短嵌入式产品开发周期的同时，保证系统高可靠性。

随着体系结构从单核模式到异构多核模式，处理对象从简单控制系统到异构信息物理融合系统的渐进演化，嵌入式系统设计的复杂性越来越高。大量的时间与资源被消耗在系统可信构造上，在时间与效率方面可信构造已经成为了系统设计的主要瓶颈。本项目基于系统设计高阶规约，研究如何提高自顶向下嵌入式设计流程中各个环节的效率，有效降低异构系统可信构造的复杂性。本项目主要研究内容与贡献如下: ..1)不确定环境下异构系统高阶规约的形式化建模与自动分析方法。基于统计模型检验技术，创新地提出了不确定环境下异构嵌入式系统性能的建模与定量评估框架，支持不确定环境下异构嵌入式设计的自动评估、比较与优化，该框架已在多个领域如异构多核片上系统、云计算与智能建筑方面得以应用。..2)基于高阶规约的自动化测试用例生成的优化方法。基于有界模型检验（Bounded Model Checking），创新地提出了一种高效的基于属性时空分解与决策序列学习的自动化测试用例生成技术， 能有效降低测试用例的总体时间，加速比可达5-10倍。..3）资源受限情况下异构高阶规约的高效综合方法。基于目前已有的分支界定方法，系统地提出了多种搜索空间约减方法来快速获取最优设计；创新地提出了基于结构的状态空间约减方法，支持除上下界比较之外新的搜索空间约减；提出了一种有效的两阶段搜索方法，支持最紧初始搜索空间的获取；提出了一种基于状态空间划分与上界投机的搜索方法，支持多搜索任务间的协同并行搜索快速获得最优解。实验结果显示，我们提出的方法比现有最好的分支界定方法快10-1000倍。..4)基于高阶规约验证结果重用的多抽象层次一致性检测方法。创新地提出了一种基于断言与测试用例重用的顶层设计与底层实现的一致性检测方法，支持自动化的将顶层规约的断言与测试用例转化为底层实现的断言与测试用例，通过轨迹比较确保系统从系统高阶规约到具体实现逐步精化过程中的一致性与正确性。.. 本项目的研究保证了在不确定环境下系统级设计的性能，大幅度降低了顶层设计到底层实现间的综合时间，提高了系统的整体测试与验证的效率，并提供了一套自动检测顶层设计与底层实现间功能一致的方法。我们的研究能够在缩短嵌入式产品开发周期的同时，保证系统高可靠性。