|
本研究では、連続時間で設計された振る舞いを離散時間環境で実行する際に生じる問題について研究を行った。CPSなどのソフトウェアでは、時間経過に応じて連続的に状態が変化するほかに、一定の条件が成立した場合には、離散的に遷移が発生する。このような振舞いはハイブリッドオートマトンでモデル化され、プログラムで実現する。しかし、プログラムは離散的なサンプリングに基づいて実行されるため、振舞いが異なる場合がある。プログラムとして関数型言語Haskellの領域特化言語であるYampaプログラムにおいて、時間オートマトンとの合成で離散動作意味をモデル化してその振舞いを検証する枠組みを提案した。
|
