基于高级逻辑的交叉算子的形式化研究

发布时间：2024-05-19 23:47

　　随着计算机系统规模的迅速增大,系统设计实现的正确性问题越来越严峻。形式化方法的出现,成为了解决该问题的一个重要手段。它运用数学方法的特点相比于传统的模拟和测试具有更高的可靠性和良好的完备性。其中,定理证明的方法因其既能验证系统规范又不受系统规模的限制而备受关注。遗传算法被越来越多的应用在安全性要求较高的领域,然而定理证明器中还未有形式化的遗传算法,这就限制了形式化方法在相关领域的应用。因此,将遗传算法形式化在HOL4系统中对扩展定理证明方法的应用领域具有重要的研究意义和实用价值。众所周知,遗传算法的求解能力取决于最关键的操作——交叉算子。因此,本文对应用最多的单点交叉和多点交叉进行了形式化。首先,本文采用高阶逻辑的方法对交叉算子进行了形式化分析,从而定义交叉算子生成子代的过程为交叉操作。通过对交叉操作的形式化抽象,提取了交叉操作的基本组成元素。这些基本元素组成了交叉操作的一般化模型,并使用高阶逻辑表示基本组成元素。基于一般化结构模型,使用双递归的方法提出了交叉操作的形式化模型,并用数学的方法描述了此模型。然后,使用形式化的交叉操作分别完成了单点交叉算子和多点交叉算子的形式化,并使用支持...

【文章页数】：79 页

【学位级别】：硕士

【部分图文】：

图２－１形式化??Ｆｉ．２－１?Ｆｏｒｍａｌｉｚａｔｉｏｎ??

所谓形式化，在逻辑学中首先要分析某一对象的组成部分及它们之间的联结关??系，然后对研究对象进行抽象并提取它的形式结构，最后用一种符号语言来表示此形??式结构，如图２－１所示。形式化从逻辑学理论发展到计算机应用，也就从符号语言描??述过渡到了使用特定工具表示的阶段。因此，在计算机领....

图２－３形式化验证的主要方法??－

系统实现??正确／错误？??图２－２系统规范和形式化验证的关系??Ｆｉｇ．２－２?Ｔｈｅ?ｒｅｌａｔｉｏｎ?ｂｅｔｗｅｅｎ?ｓｙｓｔｅｍ?ｓｐｅｃｉｆｉｃａｔｉｏｎ?ａｎｄ?ｆｏｒｍａｌ?ｖｅｒｉｆｉｃａｔｉｏｎ??图２－３为形式化验证目前主要使用的三种方法。下面将对它们的基本原....

图２－２系统规范和形式化验证的关系??

图２－２系统规范和形式化验证的关系??Ｆｉｇ．２－２?Ｔｈｅ?ｒｅｌａｔｉｏｎ?ｂｅｔｗｅｅｎ?ｓｙｓｔｅｍ?ｓｐｅｃｉｆｉｃａｔｉｏｎ?ａｎｄ?ｆｏｒｍａｌ?ｖｅｒｉｆｉｃａｔｉｏｎ??图２－３为形式化验证目前主要使用的三种方法。下面将对它们的基本原理、优势??与不足和目前面临....

图２－５模型检测的过程??Ｆｉｇ．２－５?Ｐｒｏｃｅｓｓ?ｏｆ?ｍｏｄｅｌ?ｃｈｅｃｋｉｎｇ??

?错误?＜给出反例３??图２－４等价性检验的过程??Ｆｉｇ．２－４?Ｐｒｏｃｅｓｓ?ｏｆ?ｅｑｕｉｖａｌｅｎｃｅ?ｃｈｅｃｋｉｎｇ??设计错误不仅仅出现在系统转换前后，还有一类需要关注的错误是出现在系统实??现上。模型检测是验证对象本身实现的正确性，它用有限状态机表达系统，系统性....

本文编号：3978633