| Project/Area Number |
17K19969
|
|---|
| Research Category |
Grant-in-Aid for Challenging Research (Exploratory)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Information science, computer engineering, and related fields
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
YUEN SHOJI 名古屋大学, 情報学研究科, 教授 (70230612)
|
|---|
| Project Period (FY) |
2017-06-30 – 2020-03-31
|
| Project Status |
Completed (Fiscal Year 2019)
|
| Budget Amount *help |
¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
Fiscal Year 2019: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2018: ¥2,340,000 (Direct Cost: ¥1,800,000、Indirect Cost: ¥540,000)
Fiscal Year 2017: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
|
|---|
| Keywords | 実時間性 / 連続時間 / 離散時間環境 / 時間オートマトン / ハイブリッドオートマトン / サンプリング意味論 / 関数的リアクティブプログラミング / サンプリング意味 / 到達可能性 / 実時間プログラム / ハイブリッドシステム / 離散実行 |
|---|
| Outline of Final Research Achievements |
We studied the formal treatment of the gap between continuous behaviour and discrete behaviour of software with dense-time behaviour, as seen in CPS (cyber-physical-Systems). Software for CPS implements the behaviour of hybrid automata, where discrete transitions occur along with continuous transitions. A discrete transition occurs if a specific condition holds over continuous variables. Since this hybrid behaviour cannot be directly implemented by software running on computers, a program runs discretely based on sampling. It is possible for the sampling to miss the critical moment to change the behaviour. We study Yampa programs, that is a DSL of Haskell describing hybrid automata. We modelled the discrete behaviour of a Yampa program that approximates the continuous behaviour by composing a hybrid automaton with a timed automaton, where the timed automata sample the behaviour of the hybrid automaton. We applied the model to Uppaal to check the property of a Yampa program.
|
| Academic Significance and Societal Importance of the Research Achievements |
連続的に動作するシステムに対して設計されたプログラムが実行環境が提供する離散的なサンプルのもとでどのように振舞うかを形式的に定義することで、プログラムと実行環境による複合的な問題点を形式的に定義することができるようになった。プログラムと実行環境とは個別には正しい振舞いをする場合であっても、組み合わせによって生じる不具合についての解析が可能になる。実時間性を持つプログラムが動作する条件を明確にすることによって、CPSなどにおいて厳密な安全性が要求される場面での信頼性を向上させることが可能になる。
|
