上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査

井上, 裕之; 土屋, 達弘; 菊野, 亨

このアイテムのアクセス数:100件（2022-07-08 01:27 集計）

このアイテムへのリンクには次のURLをご利用ください:http://hdl.handle.net/11094/27247

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr111_252_1	pdf	490 KB	36

論文情報

タイトル	上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査
別タイトル	K-induction-based model checking of concurrent systems with unbounded integer variables
タイトル (ヨミ)	ジョウカイ　ノ　ナイ　セイスウガタ　ヘンスウ　ヲ　ユウスル　ヘイコウ　システム　ニ　タイスル　kキノウホウ　ヲ　モチイタ　モデル　ケンサ
著者	井上, 裕之井上, 裕之
	土屋, 達弘土屋, 達弘
	菊野, 亨菊野, 亨
著者の別表記	Inoue, Hiroyuki
	Tsuchiya, Tatsuhiro
	Kikuno, Tohru
著者 (ヨミ)	イノウエ, ヒロユキ
	ツチヤ, タツヒロ
	キクノ, トオル
キーワード等	モデル検査
	k帰納法
	SMT
	並行システム
	model checking
	k-induction
	concurrent systems
抄録	モデル検査において上界のない整数型変数を有するシステムを対象とした場合,状態数は無限となるため,状態全てを個々に探索することは不可能である.そこで,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.
公開者	電子情報通信学会
公開者の別表記	The Institute of Electronics, Information and Communication Engineers
公開者 (ヨミ)	デンシ　ジョウホウ　ツウシン　ガッカイ
掲載誌名	電子情報通信学会技術研究報告. DC, ディペンダブルコンピューティング
巻	111
号	252
開始ページ	1
終了ページ	5
刊行年月	2011-10-13
ISSN	09135685
NCID	AA11645397
URL	http://hdl.handle.net/11094/27247
権利情報	Copyright © 2011 by IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. DC, ディペンダブルコンピューティング.111(252) P.1-P.5
DC.title	上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査
DCTERMS.alternative	K-induction-based model checking of concurrent systems with unbounded integer variables
DC.creator	井上, 裕之
	土屋, 達弘
	菊野, 亨
DC.creator	Inoue, Hiroyuki
	Tsuchiya, Tatsuhiro
	Kikuno, Tohru
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2011-10-13
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27247
DC.subject	モデル検査
	k帰納法
	SMT
	並行システム
	model checking
	k-induction
	concurrent systems
DCTERMS.abstract	モデル検査において上界のない整数型変数を有するシステムを対象とした場合,状態数は無限となるため,状態全てを個々に探索することは不可能である.そこで,k帰納法を用いたモデル検査によって,この無限状態の検証を行う方法を議論する.SMTソルバを用いて,上界のない整数型変数を含む式の充足可能性判定を行うことで,k帰納法を実現することができる.しかし,並行プログラムを対象とした場合,検証に時間がかかってしまうことが多い.この原因は,並行プログラムのような非同期システムでは,遷移関係を表す論理式の簡潔な表現が得られないためである.そこで本研究では,その問題を解決するため,よりコンパクトな遷移関係の式表現を用いた手法を提案する.
DCTERMS.abstract	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.
DC.rights	Copyright © 2011 by IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査
citation_author	井上, 裕之
	土屋, 達弘
	菊野, 亨
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2011-10-13
citation_journal_title	電子情報通信学会技術研究報告. DC, ディペンダブルコンピューティング
citation_volume	111
citation_issue	252
citation_firstpage	1
citation_lastpage	5
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27247
citation_keywords	モデル検査
	k帰納法
	SMT
	並行システム
	model checking
	k-induction
	concurrent systems

閲覧可能ファイル

論文情報

論文詳細を表示