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

• Item type: Trans(1)
• 公開日: 2001-02-15
• タイトル: 正則表現を用いた並列ごみ集めの抽象モデル検査
• タイトル / 言語: en
• タイトル: Abstract Model Checking of Concurrent Garbage Collection by Regular Expressions
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 電子技術総合研究所
• 著者所属: 東京大学大学院理学系研究科
• 著者所属(英): en
• 著者所属(英): Electrotechnical Laboratory
• 著者所属(英): en
• 著者所属(英): Graduate School of Science, University of Tokyo
• 著者名: 高橋, 孝一; 萩谷, 昌己
• 著者名(英): Koichi, Takahashi; Masami, Hagiya
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: モデル検査は状態空間の全探索によってシステムの検証を自動的に行う枠組みであるが，状態空間の爆発の問題をつねにかかえている．抽象モデル検査はこの問題を解決する1つの有力な技術であるが，メモリやネットワークなどのリンク構造を抽象化するための一般的な方法は知られていなかった．そこで本稿では，リンク構造を大きさによらず抽象化する方法を提案する．この方法では，リンク構造を構成するセルを，あらかじめ与えた正則表現を満たすか否かによって抽象化する．リンク構造全体は，セルを抽象化して得られる抽象セルの集合に抽象化される．この方法の有効性を示すために，並列ごみ集めの複数のアルゴリズムの抽象モデル検査を行った．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 42, 号 SIG02(PRO9), p. 61-70, 発行日 2001-02-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会