|
この研究は、実行可能形式仕様記述言語VDM-SLによるバーチャルマシンの開発を行うことと、同VDM-SLの実行に適したバーチャルマシンの仕様を策定することを目的とした。
バーチャルマシンの仕様として、バーチャルマシンのデータモデル、メモリモデル、レジスタモデル、バイトコードのインストラクションセット、実行コンテキスト（アクティベーション・レコード）およびコード領域の形式仕様を、モデル規範型形式仕様記述言語であるVDM-SLで記述した。上記の定義のうち、データモデル、メモリモデルおよびレジスタモデルはVDM-SL仕様の実行を意識した設計を行った。仕様記述は、VDM-SL向けの形式仕様記述環境ViennaTalk上で行った。
実行可能仕様によるユニットテストの記述を行い、形式仕様の記述にもユニットテストが有効であることが確認できた。バーチャルマシンの仕様に対するユニットテストをC言語に移植してC言語による実装に対するユニットテストの記述を非常に効率的に作成することができた。さらに、VDM-SL仕様とC実装の両方に同じユニットテストを適用することで、C言語のユニットテストでのエラーの原因が仕様レベルであるか実装レベルであるかを容易に判別することができ、C言語による実装の生産性が良好だった。開発の結果、VMの実装として、C言語による実装を行、x64プロセッサおよびarm32およびarm64プロセッサの3種類のプロセッサ向けにビルドし、実行させた。
バーチャルマシンの仕様記述の経験から、VDM-SL仕様のドキュメンテーションのためのツールとして、ウェブページ上で仕様の動作を実際に実行することで確認することができる、ViennaDocを開発した。また、VDM-SL仕様に対する探索的なテストを支援するための履歴ツールVDMPad-EpiLogを開発した。加えて、インタラクションに関する仕様記述の必要性から、VDM-SLによるGUIの仕様記述を可能にするViennaVisualsを開発した。
|
