文献

J-GLOBAL ID：201702273326106156   整理番号：17A1465846

IEEE.802.15.4ネットワークの解析モデルのための検証ツールとしてのPRISMモデル検査器の利用【Powered by NICT】

Using PRISM model checker as a validation tool for an analytical model of IEEE 802.15.4 networks

著者 (1件)： Kapus Tatjana (University of Maribor, Faculty of Electrical Engineering and Computer Science, Koroska c. 46, SI-2000 Maribor, Slovenia)
資料名： Simulation Modelling Practice and Theory  (Simulation Modelling Practice and Theory)
巻： 77  ページ： 367-378  発行年： 2017年 
JST資料番号： W0733A  ISSN： 1569-190X  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 通常,既存のネットワークシミュレーションツールを用いたシミュレーションやスクラッチから開発したシミュレータは,分析ネットワーク性能モデルの検証のために使用した。星型無線センサネットワークの解析モデルは,コーディネーターからの問い合わせを受けると,各センサノードは,衝突回避アルゴリズムを用いたIEEE802.15.4スロットキャリアセンス多重アクセスを実行することにより,それにデータフレームを送信する文献で提案されている。モデルは,ある時間などでデータの成功の確率計算のための表式から構成されている。式を検証するために,著者らのモデルは特別なシミュレーションプログラムを作成した。著者らの目的は,確率的モデル検査器PRISMを用いることであった。PRISMはユーザが論理式の形で探索確率約状態機械と質問の一種としてネットワークを形式的に必要とするだけである。確率を自動的に発見するとグラフ上にこのこれらを提示することができる。解析モデルからのすべての発現はPRISMを用いて検証できるように形式的にネットワークを特定する方法を示した。若干数のノードを含むネットワークでは,検証は正規モデル,シミュレーションとは対照的に,常にすべての可能なネットワーク挙動をチェック,チェックすることにより行うことができる統計的モデル検査は,大規模ネットワークに使用することができる。Copyright 2017 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： *解析モデル ,  通信網 ,  シミュレータ ,  確率モデル ,  *モデル検査 ,  多重化 ,  *IEEE ,  衝突回避 ,  *ネットワーク ,  アルゴリズム
準シソーラス用語： 大規模ネットワーク ,  センサノード ,  無線センサネットワーク ,  性能モデル ,  *PRISM , 【Automatic Indexing@JST】

著者キーワード (6件)： 通信ネットワーク ,  性能解析 ,  解析モデル ,  Validation ,  形式的仕様 ,  確率的モデル検査

分類 (1件)： 計算機シミュレーション  (JE11000H)

タイトルに関連する用語 (6件)： IEEE ,  解析モデル ,  検証 ,  ツール ,  PRISM ,  モデル検査