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

项目名称： 状态转换系统的格值量化验证方法研究

项目编号： No.61202105

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

立项/批准年度： 2013

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

项目作者： 张敏

作者单位： 华东师范大学

项目金额： 22万元

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

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

英文摘要： Formal verification is proving or disproving the correctness of software and hardware systems using formal methods of mathematics, among which bisimulation equivalence verification and model checking are two commonly used formal verification techniques.

英文关键词： Formal Method；Model Checking；Bisimulation；Complete Residuated Lattices；Statistic Probabilistic Verification