• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

A discrete execution model of dense-timed programs

Research Project

Project/Area Number 17K19969
Research Category

Grant-in-Aid for Challenging Research (Exploratory)

Allocation TypeMulti-year Fund
Research Field Information science, computer engineering, and related fields
Research InstitutionNagoya 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などにおいて厳密な安全性が要求される場面での信頼性を向上させることが可能になる。

Report

(4 results)
  • 2019 Annual Research Report   Final Research Report ( PDF )
  • 2018 Research-status Report
  • 2017 Research-status Report
  • Research Products

    (15 results)

All 2020 2019 2018 2017 Other

All Int'l Joint Research (3 results) Journal Article (6 results) (of which Int'l Joint Research: 5 results,  Peer Reviewed: 6 results,  Open Access: 3 results) Presentation (6 results)

  • [Int'l Joint Research] 華東師範大学/上海交通大学(中国)

    • Related Report
      2019 Annual Research Report
  • [Int'l Joint Research] 華東師範大学/上海交通大学(中国)

    • Related Report
      2018 Research-status Report
  • [Int'l Joint Research] NSFC(中国)

    • Related Report
      2017 Research-status Report
  • [Journal Article] Automating Time-series Safety Analysis for Automotive Control Systems Using Weighted Partial Max-SMT2020

    • Author(s)
      Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori, Shoji Yuen
    • Journal Title

      Journal of Information Processing

      Volume: 28 Issue: 0 Pages: 124-135

    • DOI

      10.2197/ipsjjip.28.124

    • NAID

      130007798629

    • ISSN
      1882-6652
    • Related Report
      2019 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] Session-ocaml: A session-based library with polarities and lenses2019

    • Author(s)
      Imai Keigo、Yoshida Nobuko、Yuen Shoji
    • Journal Title

      Science of Computer Programming

      Volume: 172 Pages: 135-159

    • DOI

      10.1016/j.scico.2018.08.005

    • Related Report
      2019 Annual Research Report 2018 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Updatable timed automata with one updatable clock2018

    • Author(s)
      Li Guoqiang、Wen Yunqing、Yuen Shoji
    • Journal Title

      Science China Information Sciences

      Volume: 61 Issue: 1 Pages: 1-14

    • DOI

      10.1007/s11432-016-9027-y

    • Related Report
      2018 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Session-ocaml: A Session-Based Library with Polarities and Lenses2017

    • Author(s)
      Imai Keigo、Yoshida Nobuko、Yuen Shoji
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 10319 Pages: 99-118

    • DOI

      10.1007/978-3-319-59746-1_6

    • ISBN
      9783319597454, 9783319597461
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Open Access / Int'l Joint Research
  • [Journal Article] Nested Timed Automata with Diagonal Constraints2017

    • Author(s)
      Wang Yuwei、Wen Yunqing、Li Guoqiang、Yuen Shoji
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 10610 Pages: 396-412

    • DOI

      10.1007/978-3-319-68690-5_24

    • ISBN
      9783319686899, 9783319686905
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Journal Article] Nested Timed Automata with Invariants2017

    • Author(s)
      Wang Yuwei、Li Guoqiang、Yuen Shoji
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 10606 Pages: 77-93

    • DOI

      10.1007/978-3-319-69483-2_5

    • ISBN
      9783319694825, 9783319694832
    • Related Report
      2017 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証2020

    • Author(s)
      中根里空,結縁祥治
    • Organizer
      日本ソフトウェア科学会第22回プログラミングおよびプログラミング言語ワークショップ PPL 2020
    • Related Report
      2019 Annual Research Report
  • [Presentation] Simulinkモデルに対するChainerRLを用いたハイブリッド頑健性に基づく時相理論仕様の不具合導出2020

    • Author(s)
      大脇亮太,結縁祥治
    • Organizer
      電子情報通信システム数理と応用研究会
    • Related Report
      2019 Annual Research Report
  • [Presentation] 離散時間実行環境におけるYampaプログラムに対するUppaalを用いた振舞い検証2019

    • Author(s)
      中根里空,結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会
    • Related Report
      2019 Annual Research Report
  • [Presentation] 離散時間実行環境におけるYampaプログラムに対するUppaalを用いた振舞い検証2019

    • Author(s)
      中根里空、結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会SS2018-52
    • Related Report
      2018 Research-status Report
  • [Presentation] 凍結クロックを持つ稠密時間プッシュダウンオートマトンの到達可能性のための記号ゾーン解析手法について2018

    • Author(s)
      結縁祥治、平岡祥
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会 SS2018-65 pp.7-12
    • Related Report
      2017 Research-status Report
  • [Presentation] 離散時間実行環境におけるYampaプログラムの振舞いモデル2017

    • Author(s)
      市橋友樹、結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会 SS2017-24 pp.19-24
    • Related Report
      2017 Research-status Report

URL: 

Published: 2017-07-21   Modified: 2021-02-19  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi