Abstract Model Checking of Concurrent Garbage Collection by Regular Expressions

IPSJ Web Site 1 Citations 14 References

Bibliographic Information

Other Title
  • 正則表現を用いた並列ごみ集めの抽象モデル検査
  • セイソクヒョウゲン オ モチイタ ヘイレツゴミ アツメ ノ チュウショウ モデル ケンサ

Search this article

Description

モデル検査は状態空間の全探索によってシステムの検証を自動的に行う枠組みであるが，状態空間の爆発の問題をつねにかかえている．抽象モデル検査はこの問題を解決する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.

Journal

Citations (1)*help

See more

References(14)*help

See more

Keywords

Details 詳細情報について

Report a problem

Back to top