九州大学学術情報リポジトリ
Kyushu University Institutional Repository
形式仕様記述における探索的モデリング
小田, 朋宏
https://doi.org/10.15017/1866375
出版情報：Kyushu University, 2017, 博士（工学）, 論文博士 バージョン：
権利関係：
（別紙様式2）
氏 名 ：小田朋宏
論 文 名 ：形式仕様記述における探索的モデリング 区 分 ：乙
論 文 内 容 の 要 旨
仕様記述の誤りはソフトウェア開発全体の生産性および信頼性に重大な影響を与えることから，
ソフトウェアシステムの開発において高品質な仕様記述およびその仕様記述に忠実な実装を作成す るための技術として，形式手法が研究され産業界において適用されている．形式仕様記述の適用は，
ソフトウェア開発全体のコストが軽減され，また，全体のコストのうち仕様記述工程の占める割合 が増加することが適用事例により知られている．これは，ソフトウェア開発全体の中でより多くの 意思決定が形式仕様記述において行われることを示しており，形式仕様記述を導入したソフトウェ ア開発全体の生産性の向上においては，形式仕様記述工程の生産性が重要になることが考えられる．
本論文では，形式仕様記述工程を探索的仕様記述と精緻化の2つの工程に切り分け，探索的仕様 記述を支援するための道具立てを提案する．探索的仕様記述は仕様記述に求められる妥当性と機能 項目の網羅性と実現可能性を獲得する工程であり，対象ドメインおよびその中でシステムが解決す べき問題を理解し，その問題に対して技術的経済的に実現可能な形で解決策として記述することが 探索的仕様記述で求められる作業である．形式仕様記述という数学的な対象を，ドメイン専門家や システムのオーナーや利用者や実装技術の専門家とのコミュニケーションや，解を記述するために 必要な創造性のために生かすことが，探索的仕様記述を支援するツールに求められる．本研究では，
探索的仕様記述を支援するツールを設計する上で考慮すべき設計指針を挙げた上で，探索的仕様記 述支援環境 ViennaTalk を開発した．ViennaTalkは，VDM-SL仕様を記述し，プロトタイプとし て実行させるためのライブラリをSmalltalk環境上に実現したものであり，探索的仕様記述を支援 するツールとして，Web IDEであるVDMPad，UIプロトタイピング環境 Lively Walk-Through， Web APIプロトタイピング環境 Webly Walk-Throughを提供する．ViennaTalkは，産業界でVDM による成功事例を持つ熟練技術者と学術研究者によって，探索的仕様記述支援環境として妥当であ ると評価された．また，ViennaTalkのコード生成器の性能と生成されたコードの可読性を評価し，
既存ツールに対して性能面および可読性での優位性を示すことで，有用性を示した．
