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

IPSJ Web Site

Bibliographic Information

Other Title
  • タジュウ Ambient Calculus ニ ヨル ブツリュウ キジュツ ニ タイスル ジャクソウモホウ トウカセイ オ モチイタ モデル ケンサ
  • Model Checking for Freight Systems Written in the Multiple Ambient Calculus Using Weak Bisimulation

Search this article

Abstract

我々はAmbient Calculus（AC）による物流システムの記述とそのモデル検査に関する研究を進めている．モデル検査において数千個規模の貨物輸送を扱おうとすると，プロセス式が巨大かつ複雑なものとなるため，状態空間爆発がおこり検証が実際上不可能になるという問題がある．これに対処するため，我々は個々の貨物の取扱いを個別のプロセス式として記述することが可能な多重AmbientCalculus（MAC）を提案し，プロセス式間の弱双模倣等価関係を導入し，その性質について議論した．本論文では，MACにより記述された物流システムのモデル検査法を提案し，それに基づくモデル検査システムについて述べる．提案する検査法では，多数の貨物に対する輸送計画を記述した式Pが，ある貨物cの輸送に関する所期の性質f(c)を満たしていることの検証を，貨物cに対する輸送計画を含むより小規模な式Qを用いて以下の2つの性質の検証に帰着させる．(i) P とQが貨物cの輸送について弱双模倣等価である（振舞いが等しい）こと，(ii) Qがf(c)を満たすこと．本論文では，この手法に基づくモデル検査システムの構築，ならびに検証実験についても述べる．

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.

Journal

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top