2019 Fiscal Year Research-status Report
Research on Virtual Machine to Support Model-based Formal Methods
| Project/Area Number |
18K18033
|
|---|
| Research Institution | Software Research Associates, Inc. (Key Technology Laboratory) |
|---|
Principal Investigator |
小田 朋宏 株式会社SRA(先端技術研究所), 先端技術研究所, 研究員 (00580383)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 形式手法 / VDM-SL / モデル規範型開発 / 仮想機械 |
|---|
| Outline of Annual Research Achievements |
本研究は、1. VMの仕様の確定、2. VMの実装、3. VM上のバイトコード開発環境の整備の3つのフェーズに分けて研究を実施する。
1. VMの仕様の確定では、VDMなどのモデル規範型形式手法に適した命令セットを同定し、VMおよび命令セットの仕様をVDM-SLで記述しデスクトップ上で動作するプロトタイプを実装する。
2. VMの実装では、特に、ARMプロセッサをターゲットとした実装を行い、IoTデバイスでの使用に耐えるパフォーマンスおよびメモリフットプリントを達成することを目標とする。
3.VM上のバイトコード開発環境の整備では、最終年度にはVMを有効に利用可能にするためのバイトコード開発環境を、VDM仕様記述環境 ViennaTalk 上に構築する。ViennaTalk 上でVMのバイトコードをターゲットとした自動生成機能を実装し、VDM仕様から自動生成したバイトコードを本VM上で動作させるとともに、ViennaTalk上にも本VMを実装することで、バイトコードをViennaTalk上でデバッグ可能にする。
本年度までに、1.および2.を遂行する計画のところ、C言語によるVMの実装を行い、ARMプロセッサ上で実行した。本年度は、ヒープ上に確保した複合値について、重複の排除によって高速化およびメモリフットプリントを小さくすることを試みた。
また、VDM-SLで記述したVMの仕様のドキュメンテーションとして、既存ツールによるLaTeXによる説明書を作成するだけでなく、VDM-SLの実行可能仕様としての特性を生かした実行可能なドキュメンテーションツールを作成し、査読付き論文1篇(英文)にまとめた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本年度実施する予定であったC言語による実装が部分的に前年度から開始していたこともあり、予定通りC言語による実装を、組み込み等でよく用いられるARMプロセッサ上で動作させた。また、計画には含まれていなかったが、VDM-SLで記述したVMの仕様について、形式仕様だけでなく自然言語によるドキュメンテーションの必要性が指摘されたことから、VDM-SLの実行可能仕様としての特性を生かした、ウェブブラウザ上でアニメーション実行可能なドキュメンテーションツールを作成し、査読付き論文1篇(英文)にまとめた。
|
| Strategy for Future Research Activity |
ARMプロセッサ上での性能向上を図るとともに、VMおよびVDM-SLからのバイトコード生成機をSmalltalk言語で実装し、ViennaTalk上で動作させる。また、VM上で動作する簡単なアプリケーションの作成を行う。
|
