|
本研究では、連続時間で設計された振る舞いを離散時間環境で実行する際に生じる問題について研究を行った。連続時間において連続的変化をするシステムの振舞いはハイブリッドオートマトンによってモデル化し、その振舞いをプログラムで記述して実行することによって実世界におけるシステムを模倣し制御する。ここで、プログラムの実行は離散的であるため、連続的な振舞いを正確に実現することはできず、離散的なサンプリングによって振舞いを近似することになる。このとき、ハイブリッドトートマトンとしては等価であっても離散的な近似では、離散的サンプリングのタイミングによって振舞いが異なる場合がある。
この現象を関数型言語HaskellのDSLとして開発されているYampaプログラムの検証の問題としてとらえた。Yampaプログラムでは、型として稠密時間Timeを持ち、Timeから値に対応する型の関数として信号を記述する。意味として連続的意味を持つため、Yampaプログラムは連続的な振舞いを記述しているが、実行環境では、一定のサンプル時間によって実行されるため、記述によってはその振舞いを実現できないことがある。枠内でボールが反発するプログラムをモデル化した場合、等価なハイブリッドオートマトンとして記述されるYampaプログラムにおいて、でイベントが近接して生起する場合、異なった振舞いが生じることがモデル検査アルゴリズムに基づいて示される。
前年度までの研究を引き続いてモデル検査器UPPAALを用いて離散的振舞いモデルにおいてモデル検査を行う際に固定小数点数を扱えるように拡張し、結果の精度を向上させた。
|
