2018 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 | 形式手法向けVM / VDM-SLによるVM開発 / レジスタマシンVMの設計 |
|---|
| Outline of Annual Research Achievements |
実行可能形式仕様記述言語VDM-SLを実行するバーチャルマシン(VM)としてViennaVMの開発を行った。計画では初年度はViennaVMのVDM-SL仕様を記述する予定だったが、実際にはViennaVMの機能のうち、メモリ管理やレジスタや演算命令、分岐命令、関数呼び出し命令など、一般のVMと共通する部分のVDM-SL仕様を記述し、C言語で実装した。VDM-SL仕様は実行可能な形式で記述され、既存のVDM-SLインタプリタVDMJによって実行することができる。その結果、フィボナッチ数を求める関数定義など、再帰関数を用いた数値演算をおこなう関数をViennaVMのIRコードで実装し、VDMJ上で動作するViennaVMで実行することを可能にした。
続いて、ViennaVMのVDM-SL仕様に基づいて、同VMをC言語で実装した。macOS(Core5i, 64ビット)およびRaspberryPi(ARM v7, 32ビット)でC言語実装をコンパイルし実行し、フィボナッチ数を求めるマイクロベンチマーキングを実施した。結果、Python 3と同等以上の性能が得られた。
上記開発に基づいて、査読付きの論文を2編（英文1編、和文1編)を出版した。さらに、現在までに開発したViennaVMのVDM-SL仕様およびC実装を https://github.com/tomooda/ViennaVM/ でオープンソースとして公開した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初目標としていたViennaVMのVDM-SL仕様の記述は概ね完了した上で、次年度に予定していたC言語による実装をおこなった。まだViennaVMに予定している機能全体の開発は完了していないが、メモリ管理、数値演算、条件分岐、再帰呼び出しなどプログラムの実行に最低限必要な機能を、現在実用されている汎用プログラミング言語処理系であるPythonと同等の性能で実装することができた。
|
| Strategy for Future Research Activity |
次年度は、IRコードの最適化や形式仕様の実行時検証のために必要な機能の仕様記述と実装を行う。現在、RaspberryPi上のARMプロセッサおよびIntelプロセッサで動作させているが、IoTでの応用に向けてリソースが限定的なシステム上での動作を目標とする。
|
| Causes of Carryover |
開発用のPCを購入する予定であったが、現在仕様している機材がまだ使用可能な状態であったため、購入を1年延期した。次年度に購入する。
|
