| 研究課題/領域番号 |
17K19969
|
|---|
| 研究種目 |
挑戦的研究(萌芽)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
情報科学、情報工学およびその関連分野
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
結縁 祥治 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| 研究期間 (年度) |
2017-06-30 – 2020-03-31
|
| 研究課題ステータス |
完了 (2019年度)
|
| 配分額 *注記 |
6,240千円 (直接経費: 4,800千円、間接経費: 1,440千円)
2019年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2018年度: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円)
2017年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
|
|---|
| キーワード | 実時間性 / 連続時間 / 離散時間環境 / 時間オートマトン / ハイブリッドオートマトン / サンプリング意味論 / 関数的リアクティブプログラミング / サンプリング意味 / 到達可能性 / 実時間プログラム / ハイブリッドシステム / 離散実行 |
|---|
| 研究成果の概要 |
本研究では、連続時間で設計された振る舞いを離散時間環境で実行する際に生じる問題について研究を行った。CPSなどのソフトウェアでは、時間経過に応じて連続的に状態が変化するほかに、一定の条件が成立した場合には、離散的に遷移が発生する。このような振舞いはハイブリッドオートマトンでモデル化され、プログラムで実現する。しかし、プログラムは離散的なサンプリングに基づいて実行されるため、振舞いが異なる場合がある。プログラムとして関数型言語Haskellの領域特化言語であるYampaプログラムにおいて、時間オートマトンとの合成で離散動作意味をモデル化してその振舞いを検証する枠組みを提案した。
|
| 研究成果の学術的意義や社会的意義 |
連続的に動作するシステムに対して設計されたプログラムが実行環境が提供する離散的なサンプルのもとでどのように振舞うかを形式的に定義することで、プログラムと実行環境による複合的な問題点を形式的に定義することができるようになった。プログラムと実行環境とは個別には正しい振舞いをする場合であっても、組み合わせによって生じる不具合についての解析が可能になる。実時間性を持つプログラムが動作する条件を明確にすることによって、CPSなどにおいて厳密な安全性が要求される場面での信頼性を向上させることが可能になる。
|
