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

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

電子情報通信学会技術研究報告. DC, ディペンダブルコンピューティング, 2011, 111(252), 1-5

Number of Access:675（2025-09-03 10:15 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27247

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr111_252_1 pdf None 490 KB 81 2014.04.03  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
上界のない整数型変数を有する並行システムに対するk帰納法を用いたモデル検査
K-induction-based model checking of concurrent systems with unbounded integer variables
ジョウカイ　ノ　ナイ　セイスウガタ　ヘンスウ　ヲ　ユウスル　ヘイコウ　システム　ニ　タイスル　kキノウホウ　ヲ　モチイタ　モデル　ケンサ
Creator
CreatorName
井上, 裕之 ; イノウエ, ヒロユキ ; Inoue, Hiroyuki
NRID
1000030283740 1000030283740
ORCID
0000-0002-3329-9235 0000-0002-3329-9235
researchmap permalink
tatsuhirotsuchiya72 tatsuhirotsuchiya72
Scopus Author ID
7403030658 7403030658
CreatorName
土屋, 達弘 ; ツチヤ, タツヒロ ; Tsuchiya, Tatsuhiro
NRID
1000050093745 1000050093745
CreatorName
菊野, 亨 ; キクノ, トオル ; Kikuno, Tohru
Subject
モデル検査
k帰納法
SMT
並行システム
model checking
k-induction
concurrent systems
Abstract
モデル検査において上界のない整数型変数を有するシステムを対象とした場合,状態数は無限となるため,状態全てを個々に探索することは不可能である.そこで,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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. DC, ディペンダブルコンピューティング
Volume (Issue)
111(252)
Page
1-5
Date of Issued
2011-10-13
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27247
PISSN
09135685
NCID
AA11645397
Access Rights
open access
CopyRight
Copyright © 2011 by IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article