Abstract Model Cheking and Its Applications

本文研究了抽象模型校核和计算系统校核的相关方法。主要成就如下：我们首先提出了一种抽象堆结构的通用方法，以便验证操作堆的算法，例如并发垃圾收集。为了表示堆上单元之间的关系，我们设计了一种使用正则表达式来描述单元之间的向前和向后连接的方法。作为抽象模型检验的一种应用，我们提出了一种分析nonce可能泄漏的分析方法，并将其与基于链空间的验证方法相结合。此外，为了分析概率攻击或拒绝服务攻击，我们引入了定时多集重写系统，并研究了它的分析方法。在通过模型检查发现算法方面，我们发现了几种用于并发垃圾收集的动态算法和快照算法。我们也试图发现互斥算法，实际上发现了Dekker算法在一些特殊条件下的一种变体。为了加快搜索速度，我们还应用了BDD（二进制决策图）。对于模型检查算法本身的验证，我们引入了一个具有图中节点间抽象关系的框架，并制定了包括覆盖图构造在内的抽象模型检查算法。我们将结果应用于时间自动机的验证。特别地，我们制定了在定价的定时自动化上寻找代价最小的状态转移路径的算法，即带代价的定时自动化，作为本研究提出的抽象算法的一个实例。我们还制定了抽象算法的A*版本，并将其应用于定价时间自动机。

This research investigated abstract model checking and related methods for verifying computational systems. Following are its major achievements.We first proposed a general method for abstracting heap structures in order to verify algorithms that manipulate heap, such as concurrent garbage collection. In order to represent relationship between cells on heap, we devised a method to use regular expressions to characterize forward and backward connections from a cell.As an application of abstract model checking, we proposed an analysis method called nonce analysis, which analyzes how nonces may leak, and combined it with the verification method based on strand spaces. In addition, in order to analyze probabilistic attacks or denial of service, we introduced the system of timed multiset rewriting and investigated its analysis methods.As for discovering algorithms by model checking, we found several variants of on-the-fly and snapshot algorithms for concurrent garbage collection. We also tried to discover mutual exclusion algorithms, and actually found a variant of Dekker's algorithm under some special conditions. We also applied BDD (binary decision diagram) in order to speed up the search.As for verification of model checking algorithms themselves, we introduced a framework with an abstraction relation among nodes in a graph, and formulated abstract model checking algorithms including covering graph construction. We applied the result to verification of timed automata. In particular, we formulated the algorithm for finding a state transition path with a minimal cost on a priced timed automation, i.e., timed automation with costs, as an instance of the abstract algorithm proposed by this research. We also formulated the A* version of the abstract algorithm and applied it to priced timed automata.