状态转换系统的格值量化验证方法研究-东篱科研大数据发现系统（DRDS）

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

状态转换系统的格值量化验证方法研究

项目名称：状态转换系统的格值量化验证方法研究
项目类别：青年科学基金项目
批准号：61202105
申请代码：F020106
项目来源：国家自然科学基金
研究期限：2013-01-01-2015-12-31

项目负责人：张敏
依托单位：华东师范大学
批准年度：2012

中文摘要：

形式化验证是使用数学方法确保计算机软硬件系统的正确性和可靠性。常用的形式化验证方法是互模拟等价验证和模型检测技术。经典的互模拟等价验证和模型检测技术是在二值逻辑上展开的。近年来，大家开始关注非二值情形的形式化验证方法研究，逐步形成了量化验证理论，包括数值量化验证方法和非数值量化验证方法。本项目提出格值互模拟理论和格值模型检测方法，形成一种新的非数值（格值）量化验证理论，其研究成果具有重要的理论意义和一定的应用价值。在前期工作基础上，本项目主要研究以下两部分内容(一)建立格值互模拟理论，探讨格值互模拟关系的重要性质，为分析系统满足其规范的(格值)量化程度提供理论依据；(二)提出格值模型检测方法，研究格值模型检测中的可判定性问题，为自动量化验证技术提供理论基础。

中文主题词：形式化方法；模型检测；互模拟关系；完备剩余格；统计概率验证

结论摘要：

英文主题词Formal Method；Model Checking；Bisimulation；Complete Residuated Lattices；Statistic Probabilistic Verification

成果综合统计