基于广义符号轨迹赋值理论的模型检测-东篱科研大数据发现系统（DRDS）

位置：立项数据库 > 立项详情页

基于广义符号轨迹赋值理论的模型检测

项目名称：基于广义符号轨迹赋值理论的模型检测
项目类别：面上项目
批准号：60973016
申请代码：F020106
项目来源：国家自然科学基金
研究期限：2010-01-01-2012-12-31

项目负责人：杨国武
负责人职称：教授
依托单位：电子科技大学
批准年度：2009

中文摘要：

广义符号轨迹赋值（GSTE）是一种针对超大规模集成化电路设计的符号轨迹赋值的推广。符号轨迹赋值在Intel、IBM和Motorola等公司得到成功的应用。广义符号轨迹赋值可以验证无限时间区间上的omega性质，在Intel得到成功应用。但它发展时间不长，还不成熟。本项目针对五个方面GSTE中断言图之间的蕴涵关系，细化与反例的产生，GSTE与传统模型检验的关系，软硬件协同验证，系统并发性质的验证，进行研究。目标是丰富GSTE理论，实现基于这些理论的高效、准确的形式化验证工具。基于语言的蕴涵关系可以转换为传统模型检验有限状态机之间的蕴涵关系。基于模型的蕴涵关系可以通过求断言图的极大模型来判断。如何在GSTE中引入SAT和按断言图作同步模拟是细化与产生反例的重要手段。比较GSTE检验方法与传统模型检验方法的差别，融合它们的优点，设计高效的形式化验证算法。同时建立软硬件统一的形式化描述方法。

中文主题词：广义符号轨迹赋值；模型检测；SAT求解器；布尔网络；

英文摘要：

Generalized Symbolic Trajector；Model checking；SAT solver；Boolean network；

英文主题词： Generalized Symbolic Trajector；Model checking；SAT solver；Boolean network；

结论摘要：

摘要广义符号轨迹赋值（GSTE）是一种针对超大规模集成化电路设计的符号轨迹赋值的推广。广义符号轨迹赋值在Intel、IBM和Motorola等公司得到成功的应用。我们研究了如下几个方面GSTE中断言图之间的蕴涵关系；细化与反例的产生；GSTE与传统模型检验的关系；嵌入式系统的仿真；SAT问题完备算法的优化；SAT求解器和BDD的应用等等。我们比较了GSTE检验方法与传统模型检验方法的差别，融合了它们的优点，设计出了高效的形式化验证算法；我们丰富了GSTE理论，实现了基于这些理论的高效、准确的形式化验证工具；同时，通过应用形式化的方法，我们验证了一些混杂系统的特性，优化了生化系统中同步布尔网络求吸引子的算法等等。

成果综合统计