|
本年度は、実時間性をもつコードとして、関数型言語のHaskellのハイブリッドシステムのDSLであるYampaを対象としてコード実行の振舞いについて研究を行った。Yampaは連続的な振舞いと条件が成立したことをチェックして離散的な振舞いを起動する。Yampaは振舞い意味としてハイブリッドシステムを記述することができるにもかかわらず、処理系の振舞いは離散的であるため、ハイブリッドシステムの実行がプログラムが持つハイブリッドシステムの振舞いと一致しない。前年度まで実施したコードを直接証明する枠組みを構築しても、実際のプログラムの振舞いが求められた性質を満たすとは限らない。この点で、コードの振舞いの離散実行意味モデルとして「差分オートマトン」を提案した。差分オートマトンは、離散的な振舞いが任意の時間で実行できることを仮定しない。連続的な振舞いから離散的振舞いに移行するために微小時間が経過することを仮定する。このことによって、ハイブリッドシステムで解釈した場合には正しく動作するはずのYampaプログラムに対して、意図しない実行パスが存在することが定式化できた。実際にYamapプログラムは実行環境の実時間性に大きな影響を受ける場合が実際に認められ、その状況を差分オートマトンでモデル化できることを示した。Yampaの機能を制限したμ-Yampaを提案し、このモデルにもとづいて、実時間プログラムの検証可能性について研究を進めた。
|
