| 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)
伊藤 恵 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30303324)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥7,500,000 (Direct Cost: ¥7,500,000)
Fiscal Year 2002: ¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 2001: ¥3,200,000 (Direct Cost: ¥3,200,000)
Fiscal Year 2000: ¥2,800,000 (Direct Cost: ¥2,800,000)
|
|---|
| Keywords | object-oriented method / embedded system / analysis model / formal method / theorem proving system / concurrent regular expression / thread / concurrent object / 組み込みシステム / 定理証明 / 形式的オブジェクト指向方法論 / オブジェクト / 実時間OS |
|---|
| 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.
|
