2020 年度研究成果報告書

モデル規範型形式手法を支援するバーチャルマシンの研究

研究課題

PDF

研究課題/領域番号	18K18033
研究種目	若手研究
配分区分	基金
審査区分	小区分60050:ソフトウェア関連
研究機関	株式会社SRA(先端技術研究所)
研究代表者	小田朋宏株式会社SRA(先端技術研究所), 先端技術研究所, 研究員 (00580383)
研究期間 (年度)	2018-04-01 – 2021-03-31
キーワード	形式手法 / 実行可能仕様 / バーチャルマシン
研究成果の概要	実行可能形式仕様記述言語VDM-SLの実行を主目的とするバーチャルマシンを、データモデル、メモリモデル、レジスタモデル、バイトコードのインストラクションセット、実行コンテキスト（アクティベーション・レコード）およびコード領域の形式仕様をVDM-SLにより記述し、C言語による実装でx64プロセッサおよびarm32およびarm64プロセッサの3種類のプロセッサ向けにビルドし、実行させた。VDM-SL仕様とC実装の両方に同じユニットテストを適用することで、C言語のユニットテストでのエラーの原因が仕様レベルであるか実装レベルであるかを容易に判別することができ、C言語による実装の生産性が良好だった。
自由記述の分野	ソフトウェア工学
研究成果の学術的意義や社会的意義	現在多くのプログラミング言語処理系がバーチャルマシンを利用している。バーチャルマシンの開発には多くの職人芸的な高度な設計実装の技術が求められている。本研究は、バーチャルマシンの開発に形式仕様を導入することで、バーチャルマシンの開発の敷居を下げることを目標にしている。