| Project/Area Number |
18K18033
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Software Research Associates, Inc. (Key Technology Laboratory) |
|---|
Principal Investigator |
Oda Tomohiro 株式会社SRA(先端技術研究所), 先端技術研究所, 研究員 (00580383)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥3,380,000 (Direct Cost: ¥2,600,000、Indirect Cost: ¥780,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2018: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 形式手法 / 実行可能仕様 / バーチャルマシン / VDM-SL / モデル規範型開発 / 仮想機械 / 形式手法向けVM / VDM-SLによるVM開発 / レジスタマシンVMの設計 |
|---|
| Outline of Final Research Achievements |
A virtual machine to execute VDM-SL specification was developed using VDM-SL. Data models, memory models, register models, instruction set, activation record, and code pages are specified and implemented. The implementation was written in C and compiled into native binaries for x64, arm32 and arm64. By porting unit tests written in VDM-SL into C, the implementation in C went very productive because the same unit tests were applied to the both VDM-SL and C, and it made very easy to identify the cause of the failure.
|
| Academic Significance and Societal Importance of the Research Achievements |
現在多くのプログラミング言語処理系がバーチャルマシンを利用している。バーチャルマシンの開発には多くの職人芸的な高度な設計実装の技術が求められている。本研究は、バーチャルマシンの開発に形式仕様を導入することで、バーチャルマシンの開発の敷居を下げることを目標にしている。
|
