论文部分内容阅读
从计算机软硬件开发的角度上看，如何确保计算机软件与硬件的正确性、可靠性和安全性是科学家们奋斗的终极目标。形式化方法用抽象的模型描绘所研究的系统、用逻辑公式描述所关注的性质，通过推导、验证等一系列技术得出软件是否可靠、安全的最终结论。模型检测技术是通过计算机查找所有可能出现的情况，进行搜索，看是否能够找到可能存在的反例，以此验证相关性质对于研究的模型是否成立。这样的方法主要用于检测模型中的漏洞，对于不满足某些性质的模型找到其出现漏洞的位置。而与之对应的另外一种方式:推理证明，则更侧重于说明这样的模型是如何满足我们所关注的性质的。推理证明具有较详细的推理过程和对应的推理规则，能够逐步地推导出最终的结论。
对于并发系统而言，多个进程间相互作用的描述和刻画，这样的情况比较复杂，需要占用大量的空间，容易引起状态爆炸的问题。为了更接近反映真实世界的实际情况，但不构成状态爆炸问题，合适的抽象技术和辅助约束就显得尤为重要。作为有效的辅助方法之一的公平性，在描述并发系统或者网络协议中，能够起到十分重要的作用。这样的考虑公平性的应用，在并发系统、无线传感器网络协议、嵌入式系统等重要领域的性质验证方面具有广泛的应用价值。基于以上的阐述，本论文主要研究如何在合理的约束和抽象的基础上，对并发系统、网络协议的活性（终止性）进行验证和分析。
论文的主要研究内容和贡献归纳如下:
(1)我们在公平的分布系统中考虑了不同强度的公平性:弱公平性、强公平性，提出了断言形式的“扩展的强公平性”，在考虑上述约束及K步约束下的限界公平性的基础上提出了“混合公平性”的概念，使得一般的安全性可以在弱公平性下得到保障。部分并发系统的活性可以通过一般情况下的强弱公平性的结合得到。而一些特殊形式:环结构下的网络协议的自稳定性，需要加入扩展的强公平性约束，从而得到保证。而混合的公平性，类似一个通用的结构，可以将前面提到的公平性中各个“最终”的因素结合细化到K（整数）步的约束。从而适用于更为广泛的系统行为描述。
(2)我们提出了一系列考虑多种公平性因素的推理证明规则，并提出了一个通用框架。并且对其可靠性和相对完备性进行了证明。与已有的相关工作相比，我们将公平性考虑为系统自带而非中途引入的，并且针对我们定义的扩展的公平性给出相应规则，并扩展到K步约束和“最终”情况的混合约束中。针对以上推理规则，我们提出了相应构造规则有效前提（辅助结构）的系列算法。并加入抽象（谓词抽象、秩抽象）使得能解决无穷状态系统的活性验证问题。
(3)针对现有的规模变化(Size-Change)终止性分析原理，我们将该原理进行扩展使用了新的结构，并考虑公平性的约束来体现某种对应关系。终止性是活性的一种特殊情况，对终止性的分析，在计算机软件正常运行中有很重要的作用。十几年来各国科学家针对2001年在POPL会议上首次提出的规模变化终止性分析原理进行了不同程度、各种方面的扩展和应用。本论文中我们首次将公平性因素考虑进来，使得对于更多的问题，如某些递归函数调用（函数返回结果作为下一次的输入）问题的终止性做进一步的分析。并且对于一些用原本的分析方法不能直接刻画的情况，运用公平性的约束，增加谓词，从而正确刻画其变量的变化规律，最终得到终止性的相关分析。