1997 Fiscal Year Final Research Report Summary
A Fundamental Research for Formal Models and Verification Techniques of Open Software
| Project/Area Number |
08458066
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
INAGAKI Yasuyoshi Grad.School of Eng., Nagoya Univ., Professor, 工学研究科, 教授 (10023079)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
KAWAGUCHI Nobuo Grad.School of Eng., Nagoya Univ., Assist.Professor, 工学研究科, 助手 (10273286)
YUEN Shoji Grad.School of Eng., Nagoya Univ., Assist.Professor, 工学研究科, 助手 (70230612)
SAKAI Masahiko Grad.School of Eng., Nagoya Univ., Assoc.Professor, 工学研究科, 助教授 (50215597)
SAKABE Toshiki Grad.School of Eng., Nagoya Univ., Professor, 工学研究科, 教授 (60111829)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Keywords | Concurrency / Communicating Processes / Formal Semantics / Programming Environment / Debuggin Procedure |
|---|
| Research Abstract |
We have investigated the appropriate formal framework for "open software" that behaves reactively on communications with the environment. Based on the communicating process model, we mainly focused on establishing the formal semantics and the verification techniques of open software. The results we have achieved are listed as follows :
(1) We proposed a timed extension to the communicating process model and derived an effecient alternative characterization for verification.
(2) We also proposed a probabilistic extension to the communication process model and derived effecient alternative characterizations for verification.
(3) We presented a general framework for "Structural Operational Semantics" specification to have the congruence and the well-definedness of "time".
(4) We investigated a logical characterization of open software by the multi-autoepistemic logic.
(5) We build a prototype programming environment for an efficient debugging based on the diagnostic information generation.
(6) We proposed a intermidiate description that can be abstracted as a LOTOS specification and also can be expanded as a C-program at the same time.
|
