| Project/Area Number |
08680393
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | Shizuoka University |
|---|
Principal Investigator |
ITOH Yukihiro Shizuoka Univ., Faculty of Information, Associate professor, 情報学部, 助教授 (20193526)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Project Status |
Completed (Fiscal Year 1997)
|
| Budget Amount *help |
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1997: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 1996: ¥1,500,000 (Direct Cost: ¥1,500,000)
|
|---|
| Keywords | Program Understanding / Domain world model / Verification of programs |
|---|
| Research Abstract |
A farmework of program understanding based on simulation on a domain world model is proposed and program verification system using the program understanding mechanism is developed through this project.
Conventional program understanding systems have knowledge about various patterns of programs and they try to understand programs by matching appropriate patterns with each part of programs. However, in order to understand programs, it is necessary to consider not only the source codes of the program but also the domain world manipulated by the program. Therefore, I design a program understanding system which has a domain world model and can simulate programs on the model. By observing the simulated domain world model, the system can grasp roles of programs.
I picked up programs to control machines written in assembly languages as a target, and construct an experimental system.
Moreover, I propose a system to verify programs by using the framework of the orogram understanding. The system has an ability to check whether a program satisfies its specification in terms of vocabularies mentioning states or motions of a machine. The system processes an example program containing about 5000 steps of instructions for electric appliances such as microwave oven, and verifies that it satisfies the specification such as "while cooking if the door opens then the oscillator should turn off".
|
