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

点击翻译按钮获取中文摘要

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