2002 Fiscal Year Final Research Report Summary
Research on construction of embedded software using formal object-oriented methods
| Project/Area Number |
12480071
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | JAPAN ADVANCED INSTITUTE OF SCIENCE AND TECHNOLOGY |
|---|
Principal Investigator |
KATAYAMA Takuya Japan Advanced Institute of Science and Technology, School of Information Science, Professor, 情報科学研究科, 教授 (70016468)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOKI Toshiaki Japan Advanced Institute of Science and Technology, School of Information Science, Associate, 情報科学研究科, 助手 (20313702)
CHERIF Adel Japan Advanced Institute of Science and Technology, School of Information Science, Associate, 情報科学研究科, 助手 (10303322)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Keywords | object-oriented method / embedded system / analysis model / formal method / theorem proving system / concurrent regular expression / thread / concurrent object |
|---|
| Research Abstract |
We studied on the application of formal object-oriented methods to the construction of embedded system. First, we studied on the environment to construct formal object-oriented analysis models, which consists of an editor for the models and a system for executing these models in a formalized UML notations, and a verification system which verifies correctness of invariants attached to class diagrams. The verification system adopts HOL system for its proof engine. Second, we studied a method of converting concurrent object models into thread models. This is based on the observation that direct execution of concurrent object models obtained from object-oriented methods is not applicable to usual embedded systems where hardware and timing constraints are so severe and conventional thread style execution is mandatory. An axiom system for the conversion is obtained.
|
