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

项目名称： 嵌入式系统验证中的覆盖率分析方法研究

项目编号： No.61402248

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 周旻

作者单位： 清华大学

项目金额： 26万元

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

中文关键词： 覆盖率；可满足性模理论；边界值分析；时序分析；

英文摘要： 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 u

英文关键词： Coverage；Satisfiability Modulo Theories；Boundary Value；Temporal Analysis；