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

2017 Fiscal Year Research-status 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

本研究では、連続的な時間経過に対して動作意味が定義されているプログラムを離散的な実行環境で正しく実行できる条件について研究する。
平成29年度は、ハイブリッドオートマトンのHaskell言語のドメイン固有言語であるYampaの離散時間動作意味を定義し、Yampaの実行において離散動作環境が与える振舞いの特性を定式化した。ここでは、Yampaプログラムの連続意味では発生しない現象が離散時間意味で発生することを示した。
Haskell言語の実行環境では、一定時間のサンプリングが保証されない。一般には、連続時間の実行意味を一定時間のサンプリングによる離散時間で十分に実行することは不可能であり、実用上の観点でも効率よく離散時間で十分な精度で連続時間意味を実現することは困難である。本研究においては、サンプリング時間をプログラムの連続意味に対応して変化させることによって効率的に精度の高い連続意味の実現を目指している。本年度は、基本的な意味を定義して全体の枠組みに対する知見を得た。
本年度で対象としたYampaプログラムは末尾再帰のみに限定されており、ハイブリッドオートマトンのモデル化を対象としたため、振舞いについては有限な状態によってモデル化できるクラスである。離散時間意味は離散時間の振舞いをするオートマトンと有限のロケーションに限定したハイブリッドオートマトンのYampaプログラムとの並行合成に基づいて離散時間意味を定式化した。

Current Status of Research Progress
Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

Haskell言語による記述とその実現意味について検討し、離散的な実行環境における問題点について整理し、通信プロセスモデルに基づいた基本的な実行モデルを構築したという点で概ね予定どおりである。Haskell言語ではランタイムのデバッグについてはさらに検討が必要である。

Strategy for Future Research Activity

平成30年度は、サンプリングシグナルの生成とYampaプログラムを連携させることによって動作の正しさを保証するための枠組みについて研究を進める。連続意味で満たすべき仕様Φを実現するサンプリングシグナル生成オートマトンの導出手法について研究する。Yampaプログラムがプッシュダウンオートマトンによってモデル化されるのに対して、サンプリングシグナルを生成するオートマトンは有限オートマトンに制限することで、到達可能性について決定的な性質を保存することを示すことを目標とする。
このことで、サンプリングシグナルが一定の条件を満たせば連続的な振舞いが離散的な振舞いによって実現できることを定式化する。

Causes of Carryover

本年度の発表にかかる旅費が見込みより少なく、また、実現モデルの検討について時間を要したことから実現のための環境について次年度に使用することとした。

  • Research Products

    (6 results)

All 2018 2017 Other

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

  • [Int'l Joint Research] NSFC(中国)

    • Country Name
      CHINA
    • Counterpart Institution
      NSFC
  • [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

    • Peer Reviewed / 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

    • 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

    • Peer Reviewed / Int'l Joint Research
  • [Presentation] 凍結クロックを持つ稠密時間プッシュダウンオートマトンの到達可能性のための記号ゾーン解析手法について2018

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

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

URL: 

Published: 2018-12-17  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi