A discrete execution model of dense-timed programs

2019 Fiscal Year Final Research Report

• 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
• 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.

Free Research Field

プログラミング言語

Academic Significance and Societal Importance of the Research Achievements

連続的に動作するシステムに対して設計されたプログラムが実行環境が提供する離散的なサンプルのもとでどのように振舞うかを形式的に定義することで、プログラムと実行環境による複合的な問題点を形式的に定義することができるようになった。プログラムと実行環境とは個別には正しい振舞いをする場合であっても、組み合わせによって生じる不具合についての解析が可能になる。実時間性を持つプログラムが動作する条件を明確にすることによって、CPSなどにおいて厳密な安全性が要求される場面での信頼性を向上させることが可能になる。