Abstract Model Cheking and Its Applications

本研究探讨抽象模型检查及相关的计算系统验证方法。本文首先提出了一种通用的堆结构抽象方法，用于验证并发垃圾收集等堆操作算法。为了表示堆上单元之间的关系，设计了一种用正则表达式来表示单元的前向和后向连接的方法，作为抽象模型检测的一种应用，提出了一种分析nonce泄漏的分析方法--nonce分析，并将其与基于串空间的验证方法相结合.另外，为了分析概率攻击和拒绝服务攻击，我们引入了定时多集重写系统，并研究了其分析方法;对于模型检测发现算法，我们发现了几种用于并发垃圾收集的on-the-fly和snapshot算法。我们还试图发现互斥算法，实际上发现了Dekker算法在某些特殊条件下的变体。在模型检测算法本身的验证方面，我们引入了一个图中节点间抽象关系的框架，并给出了包含覆盖图构造的抽象模型检测算法。我们将结果应用于时间自动机的验证。特别地，我们制定了在定价定时自动机上以最小成本找到状态转换路径的算法，即，时间自动机的成本，作为本研究提出的抽象算法的一个例子。我们还制定了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.