| Project/Area Number |
10680332
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | UNIVERSITY OF TSUKUBA |
|---|
Principal Investigator |
MIZUTANI Tetauya Assistant Professor Inst.Inform.Sci., Univ., Tsukuba, 電子・情報工学系, 講師 (70209758)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IKEDA Yasuwo Assistant Professor Dept.Inform., Saitama College, 情報処理学科, 講師 (10279599)
HOSONO Chiharu Associate Professor Inst.Inform.Sci., Univ., Tsukuba, 電子・情報工学系, 助教授 (20108294)
IGARASHI Shigeru Professor Inst.Inform.Sci., Univ., Tsukuba, 電子・情報工学系, 教授 (80027367)
SHIO Masayuki Assistant Professor Col.Comm.Dept., Tokiwa Univ., コミュニティ振興学部, 講師 (60302395)
TOMITA Kohji Researcher Agency of Ind.Sci.and Tech., METI, 産業技術総合研究所, 研究員 (80357574)
|
|---|
| Project Period (FY) |
1998 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2000: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1999: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1998: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | Verification of realtime controlled systems / Envelope theory / SOFA / Tense Arithmetic / Music information processing / エンヴェローブ理論 / 定時間システムの検証 / tense Arithemetic |
|---|
| Research Abstract |
A study of verification of realtime program systems are one of the most important fields for contemporary program theory. In this research project, the investigators have developed several verification formalisms for logical and procedual programs, named SOFA, the envelope theory and the tense arithmetic, based on the analytical semantics and the analytical equivalence theory. These are to analyze and verify programs that controls discretely certain continuously physical or other external system. Each formalism describes analysis of the wake-up time of the next action from an observation time. We obtain the actual rational time value when the next action will rise, so that verification can be easier and more precise.
The investigators have also researched music information processing as one of the examples of the realtime and highly intelligent program systems. They have developed and experimented realtime controlled performance systems. The design of these systems is essentially difficult because of the realtimeness and the fact that the nature of physical action and reaction by human soloists has not been understood well so far. Besides, especially, the acoustic grand piano has 0.5[sec.]delay of physical sound(i.e., the action of the corresponding key)after each input of MIDI event, so that the program must forecast human's performance in the accompaniment systems involving piano, which is another factor to make the design more complex and difficult. In order to cope with these situations and to solve various problems incurred upon with modern software techniques, they have represented specifications of these systems logically and verify these correctness using these formualisms.
|
