2020 Fiscal Year Final Research Report
Research on Virtual Machine to Support Model-based Formal Methods
| 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
|
| Keywords | 形式手法 / 実行可能仕様 / バーチャルマシン |
|---|
| 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.
|
| Free Research Field |
ソフトウェア工学
|
| Academic Significance and Societal Importance of the Research Achievements |
現在多くのプログラミング言語処理系がバーチャルマシンを利用している。バーチャルマシンの開発には多くの職人芸的な高度な設計実装の技術が求められている。本研究は、バーチャルマシンの開発に形式仕様を導入することで、バーチャルマシンの開発の敷居を下げることを目標にしている。
|
