エンヴェロープ理論に基づく実時間制御系の検証の研究

2000 年度 実績報告書

• 研究課題/領域番号: 11780188
• 研究機関: 常磐大学
• 研究代表者: 塩 雅之 常磐大学, コミュニティ振興学部, 専任講師 (60302395)
• キーワード: プログラム理論 / プログラム検証 / 実時間制御問題

研究概要

本研究は、我々の研究グループにより作られた実時間プログラム検証体系エンヴェロープ理論により、実時間プログラム・システムの検証系を構築し、さらに電子計算機上で自動的に行うことが目的である。エンヴェロープ理論はν理論を基にした実時間プログラム検証体系であり、ビークルの制御系や生ピアノの自動重奏システムなどの連続的に変化する外部の物理系を離散的に制御するプログラム系の検証システムである。我々の研究グループでは、他にもFAを基礎にした実時間プログラム検証体系SOFA、時制算術tense arithmetic(TA)も考案されている。エンヴェロープ理論の整備とともにこれらの体系を有機的に融合させることにより、より高度で厳密な検証を行うことを目指した。その結果、本研究では、エンヴェロープ理論に代わりTAを主として整備するとともに、これによる自動車合流問題、協調演奏システム等の具体例に対して検証・解析をするに至った。
強調演奏システムの検証では、検証を用意にするため、より形式的な言語で演奏システムの仕様を表現し、その上で検証を行った。その際、演奏データ構造もプログラミングおよび検証がしやすいものを検討し、検証を行った。
同時に、以上のことを電子計算機上で自動的に行う方法についても研究を行ったが、自動化の部分に関しては現在のところ外部に発表するような成果は得られていない。

研究成果

• [文献書誌] 五十嵐滋,水谷哲也,塩雅之: "Tense Arithmeticによる実時間知的プログラムの解析"応用数学合同研究集会報告集. 43-46 (1999)
• [文献書誌] 劉剣利,小池宏幸,水谷哲也,塩雅之,平賀瑠美,五十嵐滋: "PSYCHE:楽曲分析とその応用を中心として"第41回プログラミング・シンポジウム報告集. 21-30 (2000)
• [文献書誌] 塩雅之,五十嵐滋,水谷哲也,國広竜徳,永田恵典,船田宏聡,山下慎一郎: "実時間制御技術としての協調演奏システム"情報処理学会第60回全国大会(平成12年前期)公演論文集. 2-63-2-64 (2000)
• [文献書誌] T.Mizutani,S.Igarashi and M.Shio: "Representation of a Discretely Controlled Continuous System in Tense Arithmetic"Computing : The Australasian Theory Symposium (CATS 2001).Electronic Notes in Theoretical Computer Science 42.http://www.elsevier.nl/locate/entcs/volume42.html. (2001)