| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2009-06-03 14:50 SAT and SMT Based Model Checking of Concurrent Systems ○Tatsuhiro Tsuchiya・Tohru Kikuno（Osaka Univ.）  CST2009-4 |
|
| 抄録 | （和） | SATやSMTを用いたモデル検査について議論する．この種のモデル検査手法では，検証問題を論理式の充足可能性判定問題に帰着することで，モデル検査を実現する．近年におけるSATやSMTの関連技術の急速な進歩を背景に，このモデル検査手法は注目を集めているが，並行システムの検証に対しては有効性が限定されていた．この理由は，並行システムを対象とした場合，論理式の大きさが爆発的に大きくなってしまうためである．本研究では，並行システムに対する新しい動作セマンティクスを導入することで，この問題の解決を目指す．このセマンティクスに従うと，並行システムの動作をコンパクトな論理式で表現できるようになる．本稿では，まずこのセマンティクスを説明し，一般的な並行システムのモデルを対象として，SATやSMTに基づくモデル検査手法である有界モデル検査手法を提案する．その後，ペトリネットと整数変数を有する並行プログラムという二つの並行システムの具体例に対し，提案手法を適用する． |
| （英） | We discuss model checking that uses a SAT (satisfiability) or SMT (satisfiability modulo theory) solver. The basic idea behind this model checking approach is to reduce the model checking problem to the satisfiability problem of a formula of some logic. Recent advances in SAT and SMT solvers make this particular approach significantly attractive. However, it does not work effectively in verification of concurrent systems, because the size of the formula blows up if the system has high concurrency. To overcome this challenge, we propose a new semantics for concurrent systems. The new semantics allows a compact formula representation of the behavior of concurrent systems. In this paper, we first introduce this new semantics and bounded model checking based on it, in the context of a general model of concurrent systems. Then we apply it to two specific concurrent system models, namely Petri nets and concurrent programs using unbounded integer variables. |
|
| キーワード | （和） | モデル検査 / 並行システム / SAT / SMT / / / / |
| （英） | model checking / concurrent system / SAT / SMT / / / / | |
| 文献情報 | 信学技報, vol. 109, 2009年6月. | |
| 資料番号 | ||
| 発行日 | 2009-05-27 (CST) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | CST2009-4 |
|
| 研究会情報 | |
| 研究会 | MSS |
| 開催期間 | 2009-06-03 - 2009-06-04 |
| 開催地（和） | 摂南大学大阪センター |
| 開催地（英） | Setsunan University, Osaka Center |
| テーマ（和） | 【新型インフルエンザへの対応として中止を決定しました】ペトリネット，離散事象システム，一般 |
| テーマ（英） | Petri Net, Discrete Event System, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | MSS |
| 会議コード | 2009-06-CST |
| 本文の言語 | 英語 |
| タイトル（和） | |
| サブタイトル（和） | |
| タイトル（英） | SAT and SMT Based Model Checking of Concurrent Systems |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | 並行システム / concurrent system |
| キーワード(3)（和/英） | SAT / SAT |
| キーワード(4)（和/英） | SMT / SMT |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 土屋 達弘 / Tatsuhiro Tsuchiya / ツチヤ タツヒロ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 菊野 亨 / Tohru Kikuno / |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2009-06-03 14:50:00 |
| 発表時間 | 25分 |
| 申込先研究会 | MSS |
| 資料番号 | CST2009-4 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | no.73 |
| ページ範囲 | pp.19-23 |
| ページ数 | 5 |
| 発行日 | 2009-05-27 (CST) |
[研究会発表申込システムのトップページに戻る]