文献

J-GLOBAL ID：201602253830383756   整理番号：16A1365780

Java Pathfinderにおける弱公平性条件の実装

著者 (4件)： 太田十字光 (北陸先端科学技術大学院大 情報科学系) ,  田辺良則 (鶴見大 文) ,  田辺良則 (情報学研 先端ソフトウェア工学・国際研究セ) ,  青木利晃 (北陸先端科学技術大学院大 情報科学系)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 33rd  ページ： ROMBUNNO.IPPAN8-3  発行年： 2016年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： Java Pathfinderは,Javaバイトコードを対象としたソフトウェアモデル検査器であり,利用者による機能拡張が容易に行えるように工夫されている。基本機能では到達可能性検査のみが可能であるが,先行研究でLTL論理式によるモデル検査を行う機能の組み込みを行った。本研究では,弱公平性のもとでの活性検証が効率的に行えるように探索エンジンを改造した。弱公平性をLTL論理式で記述した場合との性能比較を行い,その有効性を確認した。(著者抄録)

シソーラス用語： *Java ,  *モデル検査 ,  計算機コード ,  可到達性 ,  公平性 ,  データ探索 ,  性能評価 ,  計算機プログラム ,  並列処理 ,  デッドロック ,  マルチスレッド ,  並列プログラム
準シソーラス用語： バイトコード ,  到達可能性

分類 (2件)： 汎用プログラミング言語  (JD03051H) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： Java ,  公平性 ,  実装