文献

J-GLOBAL ID：201502209173621120   整理番号：15A0950198

VDM++仕様から自動生成したJavaコードの振る舞い検証手法の提案

A parctical approach of behavior verification to Java code that was automatically generated from VDM++ specification

著者 (4件)： 大森洋一 (九大 大学院システム情報科学研究院) ,  林信宏 (九大 大学院システム情報科学研究院) ,  日下部茂 (九大 大学院システム情報科学研究院) ,  荒木啓二郎 (九大 大学院システム情報科学研究院)
資料名： 情報処理学会研究報告(Web)  (IPSJ Technical Report (Web))
巻： 2015  号： EMB-37  ページ： VOL.2015-EMB-37,NO.3 (WEB ONLY)  発行年： 2015年05月28日 
JST資料番号： U0451A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ソフトウェア開発の効率改善や品質向上の観点から,仕様からのプログラム自動生成の実用化が期待されている。フォーマルメソッドは仕様の無矛盾性を保証できることが知られており,ソフトウェア開発の早期段階から仕様を検証し,関係者の合意を得る有力な手法である。一方,実行するプログラムに対する検証も必要であり,フォーマルな仕様の検証とプログラムの検証の重複を排除することで,さらに開発効率を向上できると考えられる。本研究では,フォーマルな仕様記述言語VDM++を用いて記述した機能仕様から実行可能なJavaコードを自動生成する場合の検証手法を検討する。具体的にはVDM++によりソフトウェアの機能を検証し,実行プログラムの振る舞いをモデル検査ツールJPFにより検証する。すなわち,個々の機能はVDM++の仕様を満たしているが,それらを組み合わせたときに望ましくない振る舞いをしていないことを確認する手法を提案し,教科書の例題を用いた振る舞い検証の事例を示す。(著者抄録)

シソーラス用語： *仕様記述 ,  生産 ,  *自動化 ,  Java ,  *ソフトウェア開発 ,  効率化 ,  改変 ,  品質 ,  効率 ,  開発 ,  仕様記述言語
準シソーラス用語： VDM【ソフトウェア】 ,  開発効率 ,  効率改善 ,  自動生成 ,  品質向上

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (6件)： 仕様 ,  自動生成 ,  Java ,  検証 ,  手法 ,  提案