| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2011-10-20 11:00 上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査 ○井上裕之・土屋達弘・菊野 亨（阪大）  DC2011-20 |
|
| 抄録 | （和） | モデル検査において上界のない整数型変数を有するシステムを対象とした場合，状態数は無限となるため，状態全てを個々に探索することは不可能である．そこで，k 帰納法を用いたモデル検査によって，この無限状態の検証を行う方法を議論する．SMT ソルバを用いて，上界のない整数型変数を含む式の充足可能性判定を行うことで，k 帰納法を実現することができる．しかし，並行プログラムを対象とした場合，検証に時間がかかってしまうことが多い．この原因は，並行プログラムのような非同期システムでは，遷移関係を表す論理式の簡潔な表現が得られないためである．そこで本研究では，その問題を解決するため，よりコンパクトな遷移関係の式表現を用いた手法を提案する． |
| （英） | We discuss k-induction-based model checking that uses a Satisfiability Modulo Theories (SMT) solver. The state space of a system with unbounded integer variables is infinite; thus it is impossible to visit all of its states.K-induction is one of the model checking approaches that can be used to reason about such an infinite state space. In this approach, the problem of model checking is reduced to the satisfiability problem that can be solved by an SMT solver. However, this approach does not work effectively when applied to concurrent programs, because the formula representing the behaviors of systems with high concurrency tends to become very large. To overcome this problem, we propose an alternative approach that uses more compact formulas. | |
| キーワード | （和） | モデル検査 / k帰納法 / SMT / 並行システム / / / / |
| （英） | model checking / k-induction / SMT / concurrent systems / / / / | |
| 文献情報 | 信学技報, vol. 111, no. 252, DC2011-20, pp. 1-5, 2011年10月. | |
| 資料番号 | DC2011-20 | |
| 発行日 | 2011-10-13 (DC) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | DC2011-20 |
|
| 研究会情報 | |
| 研究会 | DC |
| 開催期間 | 2011-10-20 - 2011-10-20 |
| 開催地（和） | 機械振興会館 |
| 開催地（英） | |
| テーマ（和） | ネットワーク環境でのディペンダビリティ、および一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | DC |
| 会議コード | 2011-10-DC |
| 本文の言語 | 日本語 |
| タイトル（和） | 上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査 |
| サブタイトル（和） | |
| タイトル（英） | K-induction-based model checking of concurrent systems with unbounded integer variables |
| サブタイトル（英） | |
| キーワード(1)（和/英） | モデル検査 / model checking |
| キーワード(2)（和/英） | k帰納法 / k-induction |
| キーワード(3)（和/英） | SMT / SMT |
| キーワード(4)（和/英） | 並行システム / concurrent systems |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 井上 裕之 / Hiroyuki Inoue / イノウエ ヒロユキ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 土屋 達弘 / Tatsuhiro Tsuchiya / ツチヤ タツヒロ |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 菊野 亨 / Tohru Kikuno / キクノ トオル |
| 第3著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2011-10-20 11:00:00 |
| 発表時間 | 30分 |
| 申込先研究会 | DC |
| 資料番号 | DC2011-20 |
| 巻番号（vol） | vol.111 |
| 号番号（no） | no.252 |
| ページ範囲 | pp.1-5 |
| ページ数 | 5 |
| 発行日 | 2011-10-13 (DC) |
[研究会発表申込システムのトップページに戻る]