| Project/Area Number |
11780188
|
|---|
| Research Category |
Grant-in-Aid for Encouragement of Young Scientists (A)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tokiwa University (2000)
University of Tsukuba (1999) |
|---|
Principal Investigator |
塩 雅之 常磐大学, コミュニティ振興学部, 専任講師 (60302395)
|
|---|
| Project Period (FY) |
1999 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 2000: ¥400,000 (Direct Cost: ¥400,000)
|
|---|
| Keywords | プログラム理論 / プログラム検証 / 実時間制御問題 / 実時間システムの検証 / エンヴェロープ理論 / SOFA / 音楽情報処理 / Tense Arithmetic |
|---|
| Research Abstract |
本研究は、我々の研究グループにより作られた実時間プログラム検証体系エンヴェロープ理論により、実時間プログラム・システムの検証系を構築し、さらに電子計算機上で自動的に行うことが目的である。エンヴェロープ理論はν理論を基にした実時間プログラム検証体系であり、ビークルの制御系や生ピアノの自動重奏システムなどの連続的に変化する外部の物理系を離散的に制御するプログラム系の検証システムである。我々の研究グループでは、他にもFAを基礎にした実時間プログラム検証体系SOFA、時制算術tense arithmetic(TA)も考案されている。エンヴェロープ理論の整備とともにこれらの体系を有機的に融合させることにより、より高度で厳密な検証を行うことを目指した。その結果、本研究では、エンヴェロープ理論に代わりTAを主として整備するとともに、これによる自動車合流問題、協調演奏システム等の具体例に対して検証・解析をするに至った。
強調演奏システムの検証では、検証を用意にするため、より形式的な言語で演奏システムの仕様を表現し、その上で検証を行った。その際、演奏データ構造もプログラミングおよび検証がしやすいものを検討し、検証を行った。
同時に、以上のことを電子計算機上で自動的に行う方法についても研究を行ったが、自動化の部分に関しては現在のところ外部に発表するような成果は得られていない。
|
