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

2019 Fiscal Year Annual Research Report

A discrete execution model of dense-timed programs

Research Project

Project/Area Number 17K19969
Research InstitutionNagoya University

Principal Investigator

結縁 祥治  名古屋大学, 情報学研究科, 教授 (70230612)

Project Period (FY) 2017-06-30 – 2020-03-31
Keywords実時間性 / 連続時間 / 離散時間環境 / 時間オートマトン / ハイブリッドオートマトン
Outline of Annual Research Achievements

本研究では、連続時間で設計された振る舞いを離散時間環境で実行する際に生じる問題について研究を行った。連続時間において連続的変化をするシステムの振舞いはハイブリッドオートマトンによってモデル化し、その振舞いをプログラムで記述して実行することによって実世界におけるシステムを模倣し制御する。ここで、プログラムの実行は離散的であるため、連続的な振舞いを正確に実現することはできず、離散的なサンプリングによって振舞いを近似することになる。このとき、ハイブリッドトートマトンとしては等価であっても離散的な近似では、離散的サンプリングのタイミングによって振舞いが異なる場合がある。
この現象を関数型言語HaskellのDSLとして開発されているYampaプログラムの検証の問題としてとらえた。Yampaプログラムでは、型として稠密時間Timeを持ち、Timeから値に対応する型の関数として信号を記述する。意味として連続的意味を持つため、Yampaプログラムは連続的な振舞いを記述しているが、実行環境では、一定のサンプル時間によって実行されるため、記述によってはその振舞いを実現できないことがある。枠内でボールが反発するプログラムをモデル化した場合、等価なハイブリッドオートマトンとして記述されるYampaプログラムにおいて、でイベントが近接して生起する場合、異なった振舞いが生じることがモデル検査アルゴリズムに基づいて示される。
前年度までの研究を引き続いてモデル検査器UPPAALを用いて離散的振舞いモデルにおいてモデル検査を行う際に固定小数点数を扱えるように拡張し、結果の精度を向上させた。

  • Research Products

    (6 results)

All 2020 2019 Other

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

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

    • Country Name
      CHINA
    • Counterpart Institution
      華東師範大学/上海交通大学
  • [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 Pages: 124-135

    • DOI

      https://doi.org/10.2197/ipsjjip.28.124

    • 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

      https://doi.org/10.1016/j.scico.2018.08.005

    • Peer Reviewed / Open Access
  • [Presentation] サンプリング時間実行におけるUppaalを用いたYampaプログラムの振舞い検証2020

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

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

    • Author(s)
      中根里空,結縁祥治
    • Organizer
      電子情報通信学会ソフトウェアサイエンス研究会

URL: 

Published: 2021-01-27  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi