正則表現を用いた並列ごみ集めの抽象モデル検査

情報処理学会 Web Site 被引用文献1件 参考文献14件

書誌事項

タイトル別名
  • Abstract Model Checking of Concurrent Garbage Collection by Regular Expressions
  • セイソクヒョウゲン オ モチイタ ヘイレツゴミ アツメ ノ チュウショウ モデル ケンサ

この論文をさがす

説明

モデル検査は状態空間の全探索によってシステムの検証を自動的に行う枠組みであるが，状態空間の爆発の問題をつねにかかえている．抽象モデル検査はこの問題を解決する1つの有力な技術であるが，メモリやネットワークなどのリンク構造を抽象化するための一般的な方法は知られていなかった．そこで本稿では，リンク構造を大きさによらず抽象化する方法を提案する．この方法では，リンク構造を構成するセルを，あらかじめ与えた正則表現を満たすか否かによって抽象化する．リンク構造全体は，セルを抽象化して得られる抽象セルの集合に抽象化される．この方法の有効性を示すために，並列ごみ集めの複数のアルゴリズムの抽象モデル検査を行った．

Model checking, which is a framework for automatically verifying a system by enumerating its entire state space, always faces the problem of state space explosion. Although abstract model checking is considered as a promising technique for solving the problem, a general method that can abstract linked structures, such as memory or network, was not known. In this paper, we propose a method for abstracting linked structures independent of their size. By the method, each cell in a linked structure is abstracted by whether it satisfies each of the predefined regular expressions. The entire linked structure is then abstracted by a set of abstract cells, each of which is a result of abstracting a cell. For showing the effectiveness of the method, we did abstract model checking of the safety property of several algorithms for concurrent garbage collection.

収録刊行物

被引用文献 (1)*注記

もっと見る

参考文献 (14)*注記

もっと見る

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ