多重Ambient Calculusによる物流記述に対する弱双模倣等価性を用いたモデル検査

• Item type: Trans(1)
• 公開日: 2012-08-20
• タイトル: 多重Ambient Calculusによる物流記述に対する弱双模倣等価性を用いたモデル検査
• タイトル / 言語: en
• タイトル: Model Checking for Freight Systems Written in the Multiple Ambient Calculus Using Weak Bisimulation
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] プロセス代数，移動型プロセス，検証
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 近畿大学
• 著者所属: 近畿大学
• 著者所属: 近畿大学
• 著者所属(英): en
• 著者所属(英): Kinki University
• 著者所属(英): en
• 著者所属(英): Kinki University
• 著者所属(英): en
• 著者所属(英): Kinki University
• 著者名: 樋口, 昌宏; 森田, 哲平; 加藤, 暢
• 著者名(英): Masahiro, Higuchi; Teppei, Morita; Toru, Kato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 我々はAmbient Calculus（AC）による物流システムの記述とそのモデル検査に関する研究を進めている．モデル検査において数千個規模の貨物輸送を扱おうとすると，プロセス式が巨大かつ複雑なものとなるため，状態空間爆発がおこり検証が実際上不可能になるという問題がある．これに対処するため，我々は個々の貨物の取扱いを個別のプロセス式として記述することが可能な多重AmbientCalculus（MAC）を提案し，プロセス式間の弱双模倣等価関係を導入し，その性質について議論した．本論文では，MACにより記述された物流システムのモデル検査法を提案し，それに基づくモデル検査システムについて述べる．提案する検査法では，多数の貨物に対する輸送計画を記述した式Pが，ある貨物cの輸送に関する所期の性質f(c)を満たしていることの検証を，貨物cに対する輸送計画を含むより小規模な式Qを用いて以下の2つの性質の検証に帰着させる．(i) P とQが貨物cの輸送について弱双模倣等価である（振舞いが等しい）こと，(ii) Qがf(c)を満たすこと．本論文では，この手法に基づくモデル検査システムの構築，ならびに検証実験についても述べる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We are investigating the way for describing freight systems in the Ambient Calculus and constructing freight management systems based on it. We noticed the state space explosion problem that prevented us from model checking when we treated the processes representing the transporting plans for thousands of containers, even though we introduced partial order reduction methods. In order to solve the problem, we proposed the Multiple Ambient Calculus(MAC), which enables us to model freight systems by a set of formulas, introduced the weak bisimulation relation between the processes of MAC, and showed several properties of the relation. This paper proposes a verification method for freight systems written in MAC and discusses a model checking system using the method. Let P be the expression representing the transporting plan for large number of containers, f(c) be the formula representing the desirable property for a container c, and Q be the expression representing the transporting plan for the container c. The verification if P satisfies f(c) is reduced to the following two properties: (i)P is weak bisimilar to Q on the transportation of c, (ii)Q satisfies f(c). This paper also describes the construction of the model checking system based on the method and the results of several experiments using the system.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 5, 号 3, p. 50-60, 発行日 2012-08-20
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会