| Project/Area Number |
09245102
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
ITO Takayasu Tohoku University, Graduate School of Information Sciences, Professor, 大学院・情報科学研究科, 教授 (80124551)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IDA Tetsuo University of Tsukuba, Institute of Information Sciences and Electronics, Professor, 電子情報工学系, 教授 (70100047)
YONEZAKI Naoki Tokyo Institute of Technology, Graduate School of Mathematical and Computer Sciences, Professor, 大学院・情報理工学研究科, 教授 (00126286)
HAGIYA Masami University of Tokyo, Graduate School of Sciences, Professor, 大学院・理学研究科, 教授 (30156252)
TOYAMA Yoshihito Tohoku University, Research Institute of Electrical Communication, Professor, 電気通信研究所, 教授 (00251968)
SAKABE Toshiki Nagoya University, Graduate School of Engineering, Professor, 大学院・工学研究科, 教授 (60111829)
|
|---|
| Project Period (FY) |
1997 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥41,000,000 (Direct Cost: ¥41,000,000)
Fiscal Year 1999: ¥22,000,000 (Direct Cost: ¥22,000,000)
Fiscal Year 1998: ¥10,000,000 (Direct Cost: ¥10,000,000)
Fiscal Year 1997: ¥9,000,000 (Direct Cost: ¥9,000,000)
|
|---|
| Keywords | evolutionary programming mechanism / sound parallelization / verification / reactive system / temporal logic / functional logic programming / term rewriting system / linear logic / 発展的ソフトウェア / ソフトウェア仕様記述 / 論理・関数型プログラミング / 書換え型メタ計算モデル / 実時間論理 / 検証系 / 検証情報 / 発展的計算モデル / 適応的発展機構 |
|---|
| Research Abstract |
Computational environments are evolving from "sequential" into "parallel and/or distributed", and applications are evolving into the ones that require finer demands and requirements in efficiency, time, specification and verification, etc.
With this background models of evolvable computer software and their theoretical aspects were studied in this project.
A sound parallelization framework of transforming a sequential program into a parallel program that the resultant parallel program runs faster than the original sequential one was given for functional programs by T. Ito.
Verification and specification of distributed programs that evolve under internet environments are of important issues. M. Hagiya proposed an interesting idea of verification of verification methods and how to evolve verification conditions.
N. Yonezaki studied bow to specify and verify real-time reactive systems, using temporal logics and linear logic, and he gave various basic formal properties on temporal structures.
… More
T. Ida studied some basic properties of functional logic programs with applications to executable specifications, and he implemented a functional logic programming system under a distributed system.
Term rewriting systems (TRS) provide fine-grained operational mechanisms for executions of various structures, including evolvable programs and mechanisms.
T. Sakabe gave a model of adaptive TRSs. Y. Toyama gave an analysis and synthesis method of TRSs, and a powerful procedure of proving termination of TRSs.
Also, a number of interesting works on linear logic and its extensions were done, including 1) a proposal of introducing temporal linear logic (T. Ito), 2) a linear logic language with locality and temporality (K. Kobayashi), 3) a proposal of combining linear logic and concurrent TRSs for specification and verification of real-time systems (M. Okada), 4) an efficient compiler of linear logic programming language (N. Tamura). In addition, K. Kobayashi proposed a type system of distributed systems that guarantees deadlock-freedom, and S. Nishizaki proposed an environment calculus which is an extension of ML to incorporate environments into ML. Less
|
