| Project/Area Number |
12133206
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Review Section |
Science and Engineering
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology (JAIST) |
|---|
Principal Investigator |
FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IIDA Shusaku Senshu University, Lecturer, ネットワーク情報学部, 専任講師 (80338590)
OGATA Kazuhiro Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Assistant, 情報科学研究科, 助手 (30272991)
MORI Akira National Inst. of Advanced Industrial Sci. and Tech., Group Leader, サイバーアシストセンター, グループリーダー (30311682)
NAKAMURA Masaki Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Assistant, 情報科学研究科, 助手 (40345658)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Keywords | system security / system verification / unknown virus detection / authentication protocol / e-commerce protocol / formal methods / behavioral specification / CafeOBJ |
|---|
| Research Abstract |
The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation.
(1)Inspection Technology for Unknown Viruses : Based on the logics of behavioral specifications, a technology for modeling behavior s of programs and automatically inspecting their safety is developed. A virus inspection program is developed for Windows OS, and the effectiveness of developed technology has been proved.
(2) Safety Verification Technology based on Behavior Specification : By formalizing requirements and/or specifications in behavior level, a verification technology is developed which can verify the safety properties of systems in the level which is more honest to users or application logics. The technology has been applied to railway signal systems, software components, concurrent and distributed systems, and secure protocols, and is proved to be effective. In particular, verifications of several practical e-commerce protocols have been done using the technology.
(3) Model Checking Technology based on Behavioral Specification : Based on behavioral specifications, a model checking technology which is effective for software with infinite states is developed.
|
