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

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. Classic bisimulation equivalence verification and model checking have been extensively studied based on two-valued logic. Increasing attention has recently been devoted to multi-valued verification. The quantitative verification theory, including the numerical quantitative verification method and non-numerical quantitative verification method, has been formed gradually. In this project, we establish the basic methods of lattice-valued bisimulation and lattice-valued model checking based on the complete residuated lattice-valued logics, which form a new framework of non-numerical(lattice-valued) quantitative verification. All obtained results in this project have the theoritical significances and practical values...Based on our previous work, the aims of this project are as follows: (1) We establish a framework of lattice-valued bisimulation and explore its important properties, which provides a foundation for characterizing the degree of closeness between a system and its specification;(2) We propose the methods of lattice-valued model checking and discuss their decidability problems, which lay a basis for automatic quantitative verification techniques.

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

近年来，非二值情形的形式化验证方法研究成为研究热点，逐步形成了量化验证理论，包括数值量化验证方法和非数值量化验证方法。本项目提出格值互模拟理论和格值模型检测方法，形成一种新的非数值（格值）量化验证理论，其研究成果具有重要的理论意义和一定的应用价值。经过三年的研究，我们得到了以下三部分的研究成果：(一)建立格值互模拟理论，探讨格值互模拟关系的重要性质，为分析系统满足其规范的(格值)量化程度提供理论依据；(二)提出格值模型检测方法，研究格值模型检测中的可判定性问题，为自动量化验证技术提供理论基础。（三）开发实现了一个有效的量化验证工具SPAC及领域内的量化评估工具，为理论的实际应用的建立了一套可行性方案。