2018 Fiscal Year Research-status Report
A discrete execution model of dense-timed programs
| Project/Area Number |
17K19969
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| Project Period (FY) |
2017-06-30 – 2020-03-31
|
| Keywords | 実時間性 / サンプリング意味論 / ハイブリッドオートマトン / 関数的リアクティブプログラミング |
|---|
| Outline of Annual Research Achievements |
本年度は、前年度に検討したYampaプログラムに対するモデルの形式化およびその検証手法について検討を行った。YampaプログラムのサブクラスであるSimple Yampaを定義し、ハイブリッドオートマトンがテンプレートを満たすSimple Yampaプログラムに対応することを定義した。さらに、Simple Yampaプログラムのサンプリング実行モデルを定義した。ハイブリッドオートマトンに対応する連続的な意味と、サンプリング実行による離散的な意味とを定義し、その性質の違いについて研究を行った。連続的な意味に基づくYampaプログラムでは、ハイブリッドオートマトンの離散遷移が必ず可能であることが保証されるが、Yampaの実行環境は連続意味を実現することはできず、一定間隔でプログラムを少しずつ実行することで、離散的に時間遷移を発生させて連続変数の変化を計算する。Yampaの実行環境は抽象度が高く、通常では、実行の実時間性を保証することができない。このため、サンプリング周期に一定の揺れがあり、このような時間環境の不安定性を前提にプログラムを設計する必要がある。
本年度は、前年度の研究をもとに、具体的な定義とモデル検査器Uppaalを用いた検証手法を示した。結果として、Uppaalによる定義によって、サンプリング意味によって発生するエラーを実行前に指摘することができた。例として、枠内で反射するボールの振る舞い、自由落下するボールの振る舞いにおいて、初期値、サンプリングから、本来、枠や地面で反射しなければならないにもかかわらず、すり抜けていく場合が存在するかどうかということの自動チェック、また、サンプリングによる時間区切りの定数限界による無限ループの発生をモデル化することができた。
実時間性の研究では、再帰構造を含めた実時間プログラム実行における到達可能性問題について研究を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
2018年度で、形式モデルの定義を示すことができ、初歩的な自動検証の枠組みについて定式化ができ、Uppaalによる自動検証手法を具体的に示すことができた。コミュニケーションを基本とするモデルにおける時間の導入を目標として研究を進めているセッション型の実現についても基本的な結果を得ることができた。
|
| Strategy for Future Research Activity |
2018年度において、モデル検証器としてはUppaalを用いた。Uppaalはデータ型として16bitサイン付き整数しか用いることができないこと、データ構造が貧弱であることといった制約がある。このため、固定小数点構造をエンコードして検証を実施した。その一方で、制御構造を可視化する点で優れており、Yampaの離散意味による実行の問題点を指摘しやすいことを示すことができた。2019年度では、バックエンドに浮動小数点値を直接用いるような検証器を用いた検証系を導入して、Yampaプログラムの安全性について自動的に検証できる枠組みを研究する。さらに、対象となるYampaプログラムの対象を拡張して、プッシュダウンオートマトンを利用した検証手法について、研究を進める。
さらに、セッション型に対する時間経過を導入する枠組みついても引き続き、研究を進める計画である。
|
| Causes of Carryover |
2018年度までは基本的モデルの形式化に注力したため、学会発表、必要機材については予定よりも少なかったためである。
|
