文献

J-GLOBAL ID：201702230566361767   整理番号：17A1780268

経験報告:ソフトウェアモデル検査を用いた検証MPI Javaプログラム【Powered by NICT】

Experience Report: Verifying MPI Java Programs Using Software Model Checking

著者 (3件)： Ayub Muhammad Sohaib ,  Rehman Waqas Ur ,  Siddiqui Junaid Haroon
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： ISSRE  ページ： 294-304  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 並列および分散コンピューティングは,よりスケーラブルなソフトウェアの開発を可能にした。しかし,並列ソフトウエアを開発するプログラマは非決定性,データ競合とデッドロックを認識することが必要である。MPI(メッセージパッシングインタフェイス)はメッセージ指向分散アプリケーションを書くための一般的な標準である。MPIシステムにおけるいくつかのメッセージが多くの機械の一つおよび多くの可能な桁で処理することができる。非決定性MPI応用の結果に影響を与えることができる。交互結果は正しくないかも知れない。MPIアプリケーションを検証するために,すべてのこれらの可能な秩序を確認し,これらの順序付けは,正確な出力を与えるかどうかを決定する特定用途向けオラクルを使用する必要がある。MPJ ExpressはMPI標準のオープンソースJava実装である。MPI Javaプログラムのモデル検査は,それらの並列性質のために挑戦的な課題である。MPJ ExpressのJavaベースモデル,スレッドとしてモデル化した過程が,単一システムに非修飾MPI Javaプログラムを実行できるを開発した。モデルは実際のMPI Javaプログラムを実行する著者らのモデルを検証するためにカスタム聴取者を用いたJava PathFinder明示的状態ソフトウェアモデル検査器(JPF)適応することを可能にした。筆者らのアプローチの評価は,モデル検査は非常に複雑なメッセージ順序をもたらすことを不正確なシステム挙動を明らかにすることを示した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： *Java ,  プログラマ ,  *ソフトウェア ,  分散処理 ,  モデリング ,  *モデル検査 ,  応用プログラム ,  スレッド ,  非決定性 ,  デッドロック
準シソーラス用語： オープンソース ,  オラクル ,  MPI【インタフェイス】 ,  データ競合 , 【Automatic Indexing@JST】

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

タイトルに関連する用語 (7件)： 経験 ,  報告 ,  ソフトウェア ,  モデル検査 ,  検証 ,  MPI ,  Java