文献

J-GLOBAL ID：201302288707568354   整理番号：13A1368147

並行システムのミューテックスの形式的証明

Formal verification of mutex of concurrent system

著者 (2件)： YU Xian-feng (ShangLuo Univ., ShangLuo) ,  WANG Hui (ShangLuo Univ., ShangLuo)
資料名： IET Conference Publications  (IET Conference Publications)
巻： 598 Vol.2  ページ： 1077-1082  発行年： 2012年 
JST資料番号： B0665A  ISSN： 0537-9989  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： イギリス (GBR)  言語： 英語 (EN)

抄録/ポイント： 並行システムにおけるプロセス処理は,プロセスによる各種資源の共有に基づいている。そして,並行システムのモデルは,システムの研究基盤を支え,ミューテックスは,その重要な特性の一つを成す。本報では,排他的システムの数学モデル,Mutex-Modelを構築した。それによって,並行システムのミューテックス特性を分割し,分解した特性をLTL式の形式仕様に変換した。さらに,Mutex-Modelの定点理論に基づいてモデル検査を行ない,Mutex-Modelによる,モデルの精密化および改善を証明した。一方,検査アルゴリズムの状態爆発問題に対処するために,シンボリックモデル検査アルゴリズムを提案した。それは簡単で効率がよく,この問題の緩和に有効である。

シソーラス用語： *数学モデル ,  *モデル検査 ,  *並行処理 ,  モデル ,  組合せ問題 ,  システムモデル ,  ディジタル計算機 ,  理論
準シソーラス用語： Mutex-Model ,  状態爆発問題 ,  定点理論 ,  並行システム

分類 (2件)： システムモデル  (IB02000Z) ,  ディジタル計算機方式一般  (JC02010O)

タイトルに関連する用語 (2件)： 並行 ,  証明