嵌入式系统验证中的覆盖率分析方法研究

Dynamic verification (including testing and simulation) is the major approach for functional verification of both software and hardware systems. Compared with formal verification, dynamic verification suffers from its incompleteness. In practice, people use various coverage models to measure the progress of verification process by collecting the critical events as coverage points and measuring their coverage using certain coverage metric. However, the ultimate goal of verification is to assure that the system is bug-free. The relationship between coverage metric and system faults is very concerned by people from industry but is not yet well understood. Existing researches are carried out with over-simplified coverage models and the temporal behaviours of the system are rarely considered, which make them inapplicable to realistic cases. This project aims to address the above issues by taking into account the temporal behaviour of the system and employing more sophisticated coverage models and fault models in coverage analysis. More importantly, the research results will be applied to several realistic embedded cases (with hardware and software) to evaluate its effectiveness. The outcome of this project can be used to quantify the verification adequacy, evaluate the system reliability, improve the efficiency of verification.

动态验证方法（测试和模拟仿真）是验证系统功能正确性的主要方法。相比形式化验证方法，动态验证方法具有不完备性。为度量验证过程的完成度，实践中常使用各类覆盖模型来描述系统中的关键覆盖点，并且通过覆盖率来度量其被覆盖情况。但验证的最终目的是确保系统无缺陷，覆盖率和系统缺陷的关系一直是业界关注却没有完全解决的问题。已有研究中基于简化的覆盖模型和缺陷模型对缺陷覆盖率进行了分析，但由于模型假设过于简单，且分析方法没有考虑到系统的时序性，因此很难用于实际验证中。本课题拟对动态验证中的覆盖率分析展开深入研究，在考虑系统时序行为的前提下，对嵌入式系统进行自动抽象建模，得到带概率的状态变迁模型，再针对扩展的覆盖模型和缺陷模型进行覆盖率分析。本课题还研究嵌入式系统软硬件协同验证时的覆盖率分析问题，并进行案例研究。课题研究成果可用于定量度量验证指标以及度量系统可靠性，因此可用于指导验证过程，并有助于提高验证效率。

动态验证方法（测试和模拟仿真）是当前软硬件系统功能正确性验证的主要方法。相比形式化验证方法而言，动态验证方法具有不完备性。实践中经常使用各类覆盖模型来度量验证过程的完备程度。但验证的最终目的是为了确保系统无缺陷，覆盖率大小和系统潜在缺陷数量之间的关联关系一直是业界关注却没有完全解决的问题，现有的缺陷覆盖率分析方法中对覆盖模型和缺陷模型的假设过于简单，且分析方法没有考虑到系统的时序性，因此很难用于实际验证中。..本项目对动态验证中的覆盖率分析与提升方法展开深入研究，基于概率模型对系统中硬件模块的覆盖率分析方法以及软件模块的覆盖率提升方法进行协同研究，提高系统动态测试中的分析精度与覆盖度。..具体而言，本项目（1）设计了基于SMT可满足度的覆盖率分析支持技术，可用于构造带概率的抽象迁移系统。（2）实现了基于概率变迁系统的覆盖率分析，在考虑系统时序行为的前提下，对被验证系统进行抽象建模，得到带概率的状态变迁模型，再针对扩展的覆盖模型和缺陷模型进行覆盖率分析，定量度量了系统可靠性与覆盖率之间的关系。该方法有效解决了其他相关方法不考虑时序性所带来的问题，可用于指导验证过程，并有助于提高验证效率。（3）研究了针对软件单元测试的覆盖率提升方法，该方法基于演化算法对单元测试覆盖率进行自动提升，基于状态空间边界提升动态验证中的缺陷覆盖率。实验证明该方法可有效提升缺陷覆盖率。..本项目研究过程中，实现了3套嵌入式分析工具（分别针对软件、硬件），在开源和实际系统中进行了应用验证，发表高水平论文10篇（包括期刊论文5篇，会议论文5篇。有2篇论文分别发表在影响因子大于7、10的IEEE Transaction期刊上，此外还包含ASE等软件工程顶级会议论文1篇，包含COMPSAC国际学术会议2016年唯一最佳论文，论文中有2篇被分类为CCF A类），申请软件著作权1项，专利2项，培养硕士研究生2人。达到了项目立项目标。