Abstract Model Cheking and Its Applications

点击翻译按钮获取中文摘要

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.