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

2016 年度 実施状況報告書

モデルと制約に基づくソフトウェア開発に関する研究

研究課題

研究課題/領域番号 16K00094
研究機関信州大学

研究代表者

岡野 浩三  信州大学, 学術研究院工学系, 准教授 (70252632)

研究分担者 関澤 俊弦  日本大学, 工学部, 准教授 (10549314)
小形 真平  信州大学, 学術研究院工学系, 助教 (10589279)
研究期間 (年度) 2016-04-01 – 2019-03-31
キーワード自然語解析 / 要求仕様 / 形式記述 / オートマトン / モデル検査 / 形態素解析 / CYKアルゴリズム
研究実績の概要

システム構築において,高信頼性(安全性)と開発期間の短縮化の両立が大きな課題であり,このため設計仕様の品質保証が重要である.形式手法が有望手法の1 つであるが,開発現場においては自然語による仕様記述が主流であり,形式手法を導入する壁は高い.そこで,(1) 仕様記述の形式手法による仕様欠陥の発見に関する研究,(2) 表明の自動導出の研究,の上に,(3) 日本語記述された要求記述からのモデル変換技術を用いた制約指向型形式記述言語への変換技術,および(4) モデルや制約を用いたモデル駆動開発技術を統合し,総合的なソフトウェア開発技術を確立していくことをこの研究の目的とする.

本年は話題沸騰ポットを例題とした要求仕様書からの状態遷移図の変換を行うにあたり状態変数の抽出を自動化する方法を考案し実装実験を行った結果, その有用性を確認できた.
変換に際して既存の日本語の形態素解析ツールを活用し, またCYKアルゴリズムを用いた構文解析のテクニックを用いて, 精度の高い状態変数候補の抽出を可能とした. また中間情報をXML形式として保存し, 今後のより自由な解析を容易にする工夫をおこなっている. この結果を国内ワークショップで発表した.
またソフトウェア開発のモデル化後の解析事例としてモデル検査を用いたエラー解析をより使用者の理解に近いレベルで行える方法を時間オートマトンを対象に具体的な事故解析事例を対象に考案し,国際会議で発表した。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

自然語から形式記述を得るための方法論を具体的に考案かつ実装できた。
現在は状態の候補を得るところまでであるが、同様の手法を遷移の抽出にも活用できると予測しており、状態モデルの導出の見通しを得ることができたと考える。

今後の研究の推進方策

今後は全体の導出システムを完成させ、評価実験を行いたい。
また形式記述からの自然語要求記述の変換も行いたい。これにより仕様レビューの効率化が図れる。

次年度使用額が生じた理由

物品費にあてていた機器の購入を比較的大きな旅費充当のため見送ったことおよび共同研究者の旅費執行が少なかったことが大きな理由である.

次年度使用額の使用計画

当該研究に関連する国際会議参加が決まったためH29年度請求額と合わせてそれに充当する.

  • 研究成果

    (2件)

すべて 2017 2016

すべて 学会発表 (2件) (うち国際学会 1件)

  • [学会発表] Kuromoji と構文解析による要求仕様書から状態遷移系への自動変換の試み2017

    • 著者名/発表者名
      田幸玄陽,小形真平,岡野浩三,関澤俊弦
    • 学会等名
      ウィンターワークショップ2017・イン・飛騨高山
    • 発表場所
      高山 高山市民文化会館
    • 年月日
      2017-01-19 – 2017-01-20
  • [学会発表] A New Prop osal of Generating Counter -example in Model Checking Using Test Automaton2016

    • 著者名/発表者名
      Chikyu Yanagisawa, Shinpei Ogata, and Kozo Okano
    • 学会等名
      iwin2016
    • 発表場所
      Riga, Latovia
    • 年月日
      2016-08-29 – 2016-08-31
    • 国際学会

URL: 

公開日: 2018-01-16  

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

Powered by NII kakenhi