• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2018 年度 研究成果報告書

非近似的アプローチによるリアクティブシステム仕様の効率的な実現可能性判定法

研究課題

  • PDF
研究課題/領域番号 15K15969
研究種目

若手研究(B)

配分区分基金
研究分野 ソフトウェア
研究機関東京工業大学

研究代表者

島川 昌也  東京工業大学, 情報理工学院, 助教 (00749161)

研究期間 (年度) 2015-04-01 – 2019-03-31
キーワードリアクティブシステム仕様 / 実現可能性 / ω-オートマトン
研究成果の概要

リアクティブシステム仕様の実現可能性に関する検証は,仕様記述において見過ごされがちな危険な状況に陥る可能性を検出することができるが,一般に煩雑で計算コストの高い処理を伴う.本研究では,リアクティブシステム仕様の実現可能性判定の高速化を目的として,以下の事項に取り組んだ.(1) 部分的にBDDを利用して効率的に実現可能性判定手続きを実装する手法(部分シンボリック技法と呼ぶ)を開発した.この手法の最大の特長は,非近似的な実現可能性判定にも適用できることである.(2) 実現可能性判定を行う際に用いるωオートマトンをon-the-flyに簡約する手法を開発した.

自由記述の分野

形式手法

研究成果の学術的意義や社会的意義

本研究の意義は,リアクティブシステム仕様の非近似的な実現可能性判定の効率化に成功した点である.既存研究では,シンボリック技法を適用するために近似的なアプローチがとられていた.本研究では,部分シンボリック技法により非近似的な実現可能性判定手続きを効率的に実装する手法を提案し,実験により,近似的なアプローチに引けを取らない性能がでることを確認した.

URL: 

公開日: 2020-03-30  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi