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

モデル検査技術を活用したソフトウェア設計方法に関する研究

研究課題

研究課題/領域番号 21500036
研究種目

基盤研究(C)

配分区分補助金
応募区分一般
研究分野 ソフトウエア
研究機関大阪大学

研究代表者

岡野 浩三  大阪大学, 情報科学研究科, 准教授 (70252632)

研究分担者 谷口 健一   (00029513)
研究期間 (年度) 2009-04-01 – 2014-03-31
研究課題ステータス 完了 (2013年度)
配分額 *注記
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2013年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2012年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2011年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2009年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
キーワードモデル検査 / モデル / 形式手法 / 時間オートマトン / CEGAR / OCL / JML / ソフトウェア / フォーマルアプローチ / モデル駆動開発 / 表明 / CEGAR LOOP / 確率時間オートマント
研究概要

本研究では以下のことを行い、ソフトウェア設計へのフォーマルアプローチの適用可能性、有用性を調べた.
1.時間オートマトンンのCEGARloopの適用アルゴリズムの考案と評価.2. OCL-JML総合変換アルゴリズムの考案と実用性の評価.3.時間オートマトンをライントレースロボットに適用して検証の有効性を示した.4.既存ソフトウェアに対してJML記述をループ構造に対して数学的解析を行うことにより,より精度度良く自動生成する方法論を新たに提案しその有効性を示した.5.Javaのequals メソッドとhashCodeメソッドの整合性を自動検証する手法を考案し,その有効性を示した.

報告書

(6件)
  • 2013 実績報告書   研究成果報告書 ( PDF )
  • 2012 実績報告書
  • 2011 実績報告書
  • 2010 実績報告書
  • 2009 実績報告書
  • 研究成果

    (98件)

すべて 2014 2013 2012 2011 2010 2009

すべて 雑誌論文 (20件) (うち査読あり 8件) 学会発表 (78件)

  • [雑誌論文] PDGとSMTソルバを利用した表明自動導出手法の提案と評価2013

    • 著者名/発表者名
      小林和貴, 佐々木幸広, 岡野浩三, 楠本真二
    • 雑誌名

      電子情報通信学会論文誌

      巻: Vol.J96D, No.11(ソフトウェア基礎・応用特集号) ページ: 2657-2668

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Alloy Analyzerを用いた表明に関する欠陥の検出手法—JMLによる表明記述に対して—2013

    • 著者名/発表者名
      森恵弥佳, 岡野浩三, 楠本真二
    • 雑誌名

      日本ソフトウェア科学会学会誌コンピュータソフトウェア

      巻: Vol.30, No.3

    • NAID

      120005575505

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model2013

    • 著者名/発表者名
      Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.5, No.3 ページ: 147-155

    • 関連する報告書
      2013 実績報告書 2013 研究成果報告書
  • [雑誌論文] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml2013

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.5, No.2 ページ: 89-96

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml2013

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.5, No.2 ページ: 86-96

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] Alloy Analyzer を用いた表明に関する欠陥の検出手 法―JML による表明記述に対して―”2013

    • 著者名/発表者名
      森恵弥佳, 岡野浩三, 楠本真二
    • 雑誌名

      日本ソフトウェア科学会学会誌コンピュータソフトウェア

      巻: Vol.30, No.3,

    • NAID

      120005575505

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] PDG とSMT ソルバを利用した表明自 動導出手法の提案と評価2013

    • 著者名/発表者名
      小林和貴, 佐々木幸広, 岡野浩三, 楠本真二
    • 雑誌名

      電子情報通信学会論文誌

      巻: Vol.J96D, No.11 ページ: 2657-2668

    • 関連する報告書
      2013 実績報告書
    • 査読あり
  • [雑誌論文] LASP - a Learning Assistant System for Formal Proof2013

    • 著者名/発表者名
      Kiyoyuki Miyazawa, Kozo Okano, and Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society (IJIS)

      巻: vol.4, No.3

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml2013

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shinba, Kozo Okano, and Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society (IJIS)

      巻: vol.5, No.1

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model2013

    • 著者名/発表者名
      Kozo Okano, Toshifusa Sekizawa, Hiroaki Shinba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society (IJIS)

      巻: vol.5, No.1

    • 関連する報告書
      2012 実績報告書
    • 査読あり
  • [雑誌論文] LASP—a Learning Assistant System for Formal Proof2012

    • 著者名/発表者名
      Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.4, No.2 ページ: 85-92

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata2011

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.3, No.1 ページ: 11-20

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] A Visualization Technique for Unit Testing and Static Checking with Caller-Callee Relationships2011

    • 著者名/発表者名
      Yuko Muto, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      Journal of Convergences

      巻: Vol.2, No. 2 ページ: 1-8

    • 関連する報告書
      2013 研究成果報告書 2011 実績報告書
  • [雑誌論文] Daikon生成表明改善のためのテストケース自動生成手法とその評価実験2011

    • 著者名/発表者名
      宮本敬三, 堀直哉, 岡野浩三, 楠本真二
    • 雑誌名

      日本ソフトウェア科学会学会誌コンピュータソフトウェア

      巻: Vol. 28, No. 4

    • NAID

      130004549243

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] QoS Analysis of Real-time Distributed System Based on Hybrid Analysis of Probabilistic Model Checking2011

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: Vol.E94-D (フォーマルアプローチ特集号) ページ: 958-966

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata2011

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society (IJIS)

      巻: Vol.3,No.1 ページ: 11-20

    • 関連する報告書
      2011 実績報告書
    • 査読あり
  • [雑誌論文] An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop2010

    • 著者名/発表者名
      Takeshi Nagaoka, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      IEICE Transactions on Information and Systems

      巻: Vol.E93-D, No.5(フォーマルアプローチ特集号) ページ: 994-1005

    • NAID

      10026815323

    • 関連する報告書
      2013 研究成果報告書 2010 実績報告書
  • [雑誌論文] メソッドの自動生成を用いたOCLのJMLへの変換2010

    • 著者名/発表者名
      尾鷲方志, 岡野浩三, 楠本真二
    • 雑誌名

      日本ソフトウェア科学会学会誌コンピュータソフトウェア

      巻: Vol. 27, No. 2

    • NAID

      130004549165

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification2009

    • 著者名/発表者名
      Takeshi Nagaoka, Eigo Nagai, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol.1, No.2 ページ: 37-44

    • 関連する報告書
      2013 研究成果報告書
  • [雑誌論文] Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification2009

    • 著者名/発表者名
      Takeshi Nagaoka, Eigo Nagai, Kozo Okano, Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society (IJIS) Vol. 1, No. 2

      ページ: 37-44

    • 関連する報告書
      2009 実績報告書
    • 査読あり
  • [学会発表] 形式手法ツール用のスクリプト言語について2014

    • 著者名/発表者名
      岡野浩三
    • 学会等名
      ウィンターワークショッ プ2013・イン・大洗
    • 発表場所
      茨城 大洗
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Java におけるequals メソッドとhashCode メソッドの整合性の検査手法の提案2014

    • 著者名/発表者名
      榛葉浩章, 尾ノ上博樹, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術研究報告
    • 発表場所
      沖縄 那覇
    • 関連する報告書
      2013 実績報告書
  • [学会発表] AC2Uppaal : A Tool for automatic Generation of Timed Automata for Analysis of Cyber-Physical Systems2013

    • 著者名/発表者名
      Emsaib Geepalla, Behzad Bordbar, Kozo Okano, Seyedhamed Seyedali
    • 学会等名
      the proceedings of the World Congress on Internet Security (WorldCIS-2013) IEEE
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Bidirectional Translation between OCL and JML for Round-trip Engineering2013

    • 著者名/発表者名
      Hiroaki Shimba, Kentaro Hanada, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Accepted in the 5^<th> International Workshop on Empirical Software Engineering in Practice (IWESEP2013)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects2013

    • 著者名/発表者名
      Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2013 (IWIN2013)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC2013

    • 著者名/発表者名
      Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, Kozo Okano, Shinji Kusumoto, Kazuki Yoshioka
    • 学会等名
      Proceedings of International Workshop on Informatics 2013 (IWIN2013)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Empirical Experiments on Software Assertion and Qualities2013

    • 著者名/発表者名
      Kozo Okano, Kazuki Yoshioka, Shinji Kusumoto
    • 学会等名
      Symposium on Advanced Information Systems (SAIS2013)
    • 発表場所
      Copenhagen, Denmark
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] AC2Uppaal: A Tool for automatic Generation of Timed Automata forAnalysis of Cyber-Physical Systems2013

    • 著者名/発表者名
      Emsaib Geepalla, Behzad Bordbar, Kozo Okano, and Seyedhamed Seyedali
    • 学会等名
      the World Congress on Internet Security 2013
    • 発表場所
      London, UK
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Bidirectional Translation between OCL and JML for Round-trip Engineering2013

    • 著者名/発表者名
      Hiroaki Shimba, Kentaro Hanada, Kozo Okano, and Shinji Kusumoto
    • 学会等名
      International Workshop on Empirical Software Engineering in Practice 2013
    • 発表場所
      Bankok, Thai
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects2013

    • 著者名/発表者名
      Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto
    • 学会等名
      International Workshop on Informatics 2013
    • 発表場所
      Stockholm, Sweden
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Variable Coverage: A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC2013

    • 著者名/発表者名
      Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, Kozo Okano, Shinji Kusumoto, and Kazuki Yoshioka
    • 学会等名
      International Workshop on Informatics 2013
    • 発表場所
      Stockholm, Sweden
    • 関連する報告書
      2013 実績報告書
  • [学会発表] Empirical Experiments on Software Assertion and Qualities2013

    • 著者名/発表者名
      Kozo Okano, Kazuki Yoshioka, and Shinji Kusumoto
    • 学会等名
      Symposium on Advanced Information Systems 2013
    • 発表場所
      Copenhagen, Denmark
    • 関連する報告書
      2013 実績報告書
  • [学会発表] SMT ソルバと統計解析を用いたJava プログラ ム解析器の提案2013

    • 著者名/発表者名
      佐々木幸広,岡野浩三,楠本真二
    • 学会等名
      第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加 賀
    • 発表場所
      石川 加賀
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 制約記述言語OCL とJML の双方向変換手法の提 案2013

    • 著者名/発表者名
      榛葉浩章,岡野浩三,楠本真二
    • 学会等名
      第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
    • 発表場所
      石川 加賀
    • 関連する報告書
      2013 実績報告書
  • [学会発表] UML/OCL を用いたテスト自動生成手法のカバレッ ジ向上に関する一手法の提案2013

    • 著者名/発表者名
      藤田悠矢,岡野浩三,楠本真二
    • 学会等名
      第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
    • 発表場所
      石川 加賀
    • 関連する報告書
      2013 実績報告書
  • [学会発表] concolic execution を用いたバグ同定に関する研究2013

    • 著者名/発表者名
      大田崇史,岡野浩三,楠本真二
    • 学会等名
      第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
    • 発表場所
      石川 加賀
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 高位ソフトウェア設計検証をめざして2013

    • 著者名/発表者名
      岡野浩三
    • 学会等名
      高度情報シンポジウム2013
    • 発表場所
      北海道 知床
    • 関連する報告書
      2013 実績報告書
  • [学会発表] PDG とSMT ソルバを用いたJava プログラム解析 器の提案2013

    • 著者名/発表者名
      佐々木幸広, 岡野浩三, 楠本真二
    • 学会等名
      SES2013 併設ワークショップ プログラム・デバッグ自動化の現状と今後
    • 発表場所
      東京
    • 関連する報告書
      2013 実績報告書
  • [学会発表] ウィンターワークショップ2013・イン・那須報告2013

    • 著者名/発表者名
      野田夏子, 岡野浩三, 早水公二, 戸田航史, 上野秀剛, 石尾隆, 林晋平, 妻木俊彦, 中村匡 秀, 岸知二, 本橋正成, 鷲崎弘宜
    • 学会等名
      情報処理学会研究報告
    • 発表場所
      東京
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 異なるスキーマ間に対応するSQL 文の整合性のAlloy Analyzer を用いた一検証手法2013

    • 著者名/発表者名
      藤田悠矢, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術研究報告
    • 発表場所
      北海道 札幌
    • 関連する報告書
      2013 実績報告書
  • [学会発表] 契約記述の変更傾向の開発履歴情報を用いた調査2013

    • 著者名/発表者名
      吉岡一樹,岡野浩三,楠本真二:
    • 学会等名
      電子情報通信学会技術報告, Vol.112, No.458, pp.121-126
    • 発表場所
      志賀島休暇村(福岡県)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] 在庫管理プログラムに対するAlloy Analyzer を用 いた検証事例2013

    • 著者名/発表者名
      森恵弥佳,岡野浩三,楠本真二
    • 学会等名
      ウィンターワークショップ2013・イン・那須
    • 発表場所
      ラフォーレ那須(栃木県)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] 制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案2012

    • 著者名/発表者名
      榛葉浩章, 花田健太郎, 岡野浩三
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      沖縄
    • 年月日
      2012-03-13
    • 関連する報告書
      2011 実績報告書
  • [学会発表] SMTソルバーとPDG作成ツールを用いたJavaのテストケース自動導出手法の提案2012

    • 著者名/発表者名
      佐々木幸広, 小林和貴, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      沖縄
    • 年月日
      2012-03-13
    • 関連する報告書
      2011 実績報告書
  • [学会発表] OCLからJMLへのDSLを用いた変換ツールの試作型の実装2012

    • 著者名/発表者名
      花田健太郎, 岡野浩三, 楠本真
    • 学会等名
      ウインターワークショップ2012・イン・琵琶湖
    • 発表場所
      長浜
    • 年月日
      2012-01-20
    • 関連する報告書
      2011 実績報告書
  • [学会発表] JMLによって記述された契約に対する品質評価手法の在庫管理プログラムへの適用2012

    • 著者名/発表者名
      吉岡一樹, 武藤祐子, 岡野浩三, 楠本真二
    • 学会等名
      ウインターワークショップ2012・イン・琵琶湖
    • 発表場所
      長浜
    • 年月日
      2012-01-20
    • 関連する報告書
      2011 実績報告書
  • [学会発表] 大学での形式手法の教育の一報告2012

    • 著者名/発表者名
      岡野浩三
    • 学会等名
      ウインターワークショップ2012・イン・琵琶湖
    • 発表場所
      長浜
    • 年月日
      2012-01-20
    • 関連する報告書
      2011 実績報告書
  • [学会発表] ライントレーサの定量的評価および検証に向けて2012

    • 著者名/発表者名
      河井秀樹, 岡野浩三, 関潭俊弦
    • 学会等名
      ウインターワークショップ2012・イン・琵琶湖
    • 発表場所
      長浜
    • 年月日
      2012-01-20
    • 関連する報告書
      2011 実績報告書
  • [学会発表] Verification of Spatio-Temporal Role Based Access Control using Timed Automata,"In Proceedings of IEEE International Workshop on Design2012

    • 著者名/発表者名
      Emsaieb Geepalla, Behzad Bordbar, Kozo Okano
    • 学会等名
      Analysis and Tools for Integrated Circuits and Systems
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Verification of Safety Property of Line Tracer Program Using Timed Automaton Model2012

    • 著者名/発表者名
      Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2012 (IWIN2012)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Implementation of a Prototype Bi-Directinal Translation Tool between Ocl and Jml2012

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2012 (IWIN2012)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Practical Application of a Translation Tool from Uml/Ocl to Java Skeleton with Jml Annotation2012

    • 著者名/発表者名
      Kentaro Hanada, Kozo Okano, Shinji Kusumoto, Kiyoyuki Miyazawa
    • 学会等名
      Proceedings of 14th International Conference on Enterprise Information Systems (ICEIS2012)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] A Bi-directional Translation Tool between OCL and JML considering Reverse Translation2012

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
    • 学会等名
      The 4th International Workshop on Empirical Software Engineering in Practice (IWESEP2012)
    • 発表場所
      Osaka Japan (poster presentation)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] SMTを活用したJavaプログラム解析フレームワークの設計2012

    • 著者名/発表者名
      佐々木幸広, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第19回ワークショップFOSE2012
    • 発表場所
      (レクチャーノート・ソフトウェア学38ソフトウェア工学の基礎XI)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Practical Application of a Translation Tool from Uml/Ocl to Java Skeleton with Jml Annotation2012

    • 著者名/発表者名
      Kentaro Hanada, Kozo Okano, Shinji Kusumoto, and Kiyoyuki Miyazawa
    • 学会等名
      14th International Conference on Enterprise Information Systems
    • 発表場所
      Poland
    • 関連する報告書
      2012 実績報告書
  • [学会発表] Implementation of a Prototype Bi-Directinal Translation Tool between Ocl and Jml,2012

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shinba, Kozo Okano, and Shinji Kusumoto
    • 学会等名
      International Workshop on Informatics 2012
    • 発表場所
      France
    • 関連する報告書
      2012 実績報告書
  • [学会発表] Verification of Safety Property of Line Tracer Program Using Timed Automaton Model2012

    • 著者名/発表者名
      Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto
    • 学会等名
      International Workshop on Informatics 2012
    • 発表場所
      France
    • 関連する報告書
      2012 実績報告書
  • [学会発表] A Bi-directional Translation Tool between OCL and JML considering Reverse Translation2012

    • 著者名/発表者名
      Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto
    • 学会等名
      The 4th InternationalWorkshop on Empirical Software Engineering in Practice (IWESEP2012)
    • 発表場所
      大阪大学(大阪府)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] SMT を活用したJava プログラム解析フレーム ワークの設計2012

    • 著者名/発表者名
      佐々木幸広,岡野浩三,楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16 回 8 ワークショップFOSE2012
    • 発表場所
      ゆふいん山水館(大分県)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] UPPAAL によるライント レーサの安全性検証のケーススタディ2012

    • 著者名/発表者名
      岡野浩三,関澤俊弦,花田健太郎,榛葉浩章,楠本真二:
    • 学会等名
      SES2012 併設ワークショップ (WS-4) 形式 手法の今と未来
    • 発表場所
      東京電機大学(東京都)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] OCL との比較を用いた形式仕様記述言語JML の 品質評価メトリクスの提案2012

    • 著者名/発表者名
      吉岡一樹,岡野浩三,楠本真二
    • 学会等名
      SES2012 併設ワークショップ (WS-4) 形式 手法の今と未来
    • 発表場所
      東京電機大学(東京都)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] ウィンター ワークショップ2012・イン・琵琶湖開催報告2012

    • 著者名/発表者名
      丸山勝久,大森隆行,井垣宏,中村匡秀,伏田享平,角田雅照,風戸広史,岡田譲二, 岡野浩三,坂本一憲,本橋正成,岸知二,野田夏子,小林隆志,林晋平
    • 学会等名
      情報処理学会研究報告, Vol.2012-SE-178, No.11
    • 発表場所
      琵琶湖コンファレンスセンター(滋賀県)
    • 関連する報告書
      2012 実績報告書
  • [学会発表] Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton2011

    • 著者名/発表者名
      Kozo Okano, Behzad Bordbar, Takeshi Nagaoka
    • 学会等名
      2nd International Conference on Networking and Computing
    • 発表場所
      Osaka
    • 年月日
      2011-12-02
    • 関連する報告書
      2011 実績報告書
  • [学会発表] 呼び出し関係を用いた単体テストおよび静的検査の可視化手法の改善とその評価2011

    • 著者名/発表者名
      武藤祐子, 岡野浩三, 楠本真二
    • 学会等名
      「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2011
    • 発表場所
      青森
    • 年月日
      2011-11-25
    • 関連する報告書
      2011 実績報告書
  • [学会発表] Improvement of a Visualization Technique for the Passage Rate of Unit Testing and Static Checking and its Evaluation2011

    • 著者名/発表者名
      Yuko Mutoh, Kozo Okano, Shinji Kusumoto
    • 学会等名
      The Joint Conference of the 21th International Workshop on Software Measurement (IWSM) and the 6th International Conference on Software Process and Product Measurement (Mensura)
    • 発表場所
      Nara
    • 年月日
      2011-11-03
    • 関連する報告書
      2011 実績報告書
  • [学会発表] JMLによって記述された契約に対する品質評価手法の提案2011

    • 著者名/発表者名
      武藤祐子, 岡野浩三, 楠本真二
    • 学会等名
      平成23年度情報処理学会関西支部支部大会
    • 発表場所
      大阪
    • 年月日
      2011-09-22
    • 関連する報告書
      2011 実績報告書
  • [学会発表] Daikonを利用した表明動的生成改善手法の実プロジェクト教材への適用実験とテストデータ生成改善手法の検討2011

    • 著者名/発表者名
      小林和貴, 岡野浩三, 楠本真二
    • 学会等名
      平成23年度情報処理学会関西支部支部大会
    • 発表場所
      大阪
    • 年月日
      2011-09-22
    • 関連する報告書
      2011 実績報告書
  • [学会発表] LASP-a Learning Assistant System for Formal Proof2011

    • 著者名/発表者名
      Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
    • 学会等名
      International Workshop on INformatics, IWIN 2011
    • 発表場所
      Venice
    • 年月日
      2011-09-20
    • 関連する報告書
      2011 実績報告書
  • [学会発表] モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価2011

    • 著者名/発表者名
      小林和貴, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      札幌
    • 年月日
      2011-07-30
    • 関連する報告書
      2011 実績報告書
  • [学会発表] A Visualization Technique for the Passage Rate of Unit Testing and Static Checking with Caller-Callee Relationships2011

    • 著者名/発表者名
      Yuko Mutoh, Kozo Okano, Shinji Kusumoto
    • 学会等名
      International Conference on Advanced Software Engineering 2011
    • 発表場所
      Pusan
    • 年月日
      2011-05-27
    • 関連する報告書
      2011 実績報告書
  • [学会発表] 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法2011

    • 著者名/発表者名
      田中俊彰, 長岡武志, 岡野浩三, 楠本真二
    • 学会等名
      情報処理学会研究報告
    • 発表場所
      東京
    • 年月日
      2011-03-15
    • 関連する報告書
      2010 実績報告書
  • [学会発表] OCLからJMLへの変換ツールにおける対応クラスの拡張と教務システムに対する適用実験2011

    • 著者名/発表者名
      宮澤清介, 花田健太郎, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      沖縄
    • 年月日
      2011-03-08
    • 関連する報告書
      2010 実績報告書
  • [学会発表] Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton2011

    • 著者名/発表者名
      Kozo Okano, Behzad Bordbar, Takeshi Nagaoka
    • 学会等名
      proceedings of the 2nd International Conference on Networking and Computing
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] LASP - a Learning Assistant System for Formal Proof2011

    • 著者名/発表者名
      Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2011 (IWIN2011)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Improvement of a Visualization Technique for the Passage Rate of Unit Testing and Static Checking and its Evaluation2011

    • 著者名/発表者名
      Yuko Muto, Kozo Okano, Shinji Kusumoto
    • 学会等名
      proceedings of The Joint Conference of the 21th International Workshop on Software Measurement (IWSM2011) and the 6th International Conference on Software Process and Product Measurement (Mensura)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] A Visualization Technique for the Passage Rate of Unit Testing and Static Checking with Caller-Callee Relationships2011

    • 著者名/発表者名
      Yuko Muto, Kozo Okano, Shinji Kusumoto
    • 学会等名
      International Conference on Advanced Software Engineering 2011
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] 呼び出し関係を用いた単体テストおよび静的検査の可視化手法の改善とその評価2011

    • 著者名/発表者名
      武藤祐子, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第18回ワークショップFOSE2011
    • 発表場所
      (レクチャーノート・ソフトウェア学37ソフトウェア工学の基礎XVIII)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] アサーション動的生成を目的としたテストケース制約のESC/Java2を利用した導出2011

    • 著者名/発表者名
      小林和貴, 宮本敬三, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第17回ワークショップFOSE2010
    • 発表場所
      (レクチャーノート・ソフトウェア学36ソフトウェア工学の基礎VII)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] アサーション動的生成を目的としたテストケース制約のESC/Java2を利用した導出2010

    • 著者名/発表者名
      小林和貴, 宮本敬三, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2010
    • 発表場所
      新潟
    • 年月日
      2010-11-19
    • 関連する報告書
      2010 実績報告書
  • [学会発表] 時間システムの到達可能性解析の並列手法と評価実験2010

    • 著者名/発表者名
      田中俊彰, 長岡武志, 岡野浩三, 楠本真二
    • 学会等名
      情報処理学会研究報告
    • 発表場所
      大阪大学
    • 年月日
      2010-11-12
    • 関連する報告書
      2010 実績報告書
  • [学会発表] OCLのJMLへの変換ツールの実装と評価2010

    • 著者名/発表者名
      宮澤清介, 岡野浩三, 楠本真二
    • 学会等名
      情報処理学会研究報告
    • 発表場所
      大阪大学
    • 年月日
      2010-11-12
    • 関連する報告書
      2010 実績報告書
  • [学会発表] 時間システムの到達可能性解析の並列手法と評価実験2010

    • 著者名/発表者名
      田中俊彰, 長岡武志, 岡野浩三, 楠本真二
    • 学会等名
      平成22年度情報処理学会関西支部支部大会
    • 発表場所
      大阪
    • 年月日
      2010-09-22
    • 関連する報告書
      2010 実績報告書
  • [学会発表] 数理論理学の形式証明に対する学習支援システムの試作と評価2010

    • 著者名/発表者名
      宮澤清介, 岡野浩三, 楠本真二
    • 学会等名
      平成22年度情報処理学会関西支部支部大会
    • 発表場所
      大阪
    • 年月日
      2010-09-22
    • 関連する報告書
      2010 実績報告書
  • [学会発表] Reachability Analysis of Probabilistic Real-Time Systems Based on CEGAR for Timed Automata2010

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
    • 学会等名
      International Workshop on INformatics, IWIN 2010
    • 発表場所
      エジンバラ英国
    • 年月日
      2010-09-13
    • 関連する報告書
      2010 実績報告書
  • [学会発表] クラス間関係を利用した単体テストおよび静的検査の網羅率可視化手法2010

    • 著者名/発表者名
      武藤祐子, 岡野浩三, 楠本真二
    • 学会等名
      情報処理学会ソフトウェア工学研究会ワークショップSES2010
    • 発表場所
      東洋大
    • 年月日
      2010-09-01
    • 関連する報告書
      2010 実績報告書
  • [学会発表] OCLのJMLへの変換ツールの実装2010

    • 著者名/発表者名
      宮澤清介, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      北海道大学
    • 年月日
      2010-08-06
    • 関連する報告書
      2010 実績報告書
  • [学会発表] 実時間システムを対象としたCEGARによる抽象洗練の並列化手法2010

    • 著者名/発表者名
      田中俊彰, 長岡武志, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      北海道大学
    • 年月日
      2010-08-05
    • 関連する報告書
      2010 実績報告書
  • [学会発表] 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析2010

    • 著者名/発表者名
      伊藤明彦, 長岡武志, 岡野浩三, 楠本真二
    • 学会等名
      電子情報通信学会技術報告
    • 発表場所
      鹿児島
    • 年月日
      2010-03-08
    • 関連する報告書
      2009 実績報告書
  • [学会発表] Reachability Analysis of Probabilistic Timed Automata Based on an Abstraction Refinement Technique2010

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
    • 学会等名
      International Workshop on Empirical Software Engineering in Practice 2010
    • 関連する報告書
      2013 研究成果報告書 2010 実績報告書
  • [学会発表] Reachability Analysis of Probabilistic Real-Time Systems Based on CEGAR for Timed Automata2010

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2010 (IWIN2010)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] クラス間関係を利用した単体テストおよび静的検査の網羅率可視化手法2010

    • 著者名/発表者名
      武藤祐子, 岡野浩三, 楠本真二:
    • 学会等名
      情報処理学会ソフトウェア工学研究会ワークショップSES2010,ソフトウェアエンジニアリング最前線2010
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] アサーション動的生成のためのテストケース自動生成手法の生成アサーションの妥当性評価2010

    • 著者名/発表者名
      宮本敬三, 堀直哉, 岡野浩三, 楠本真二, 西本哲
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
    • 発表場所
      (レクチャーノート・ソフトウェア学35ソフトウェア工学の基礎XVI)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Qualitative Analysis of Real-time Distributed Systems Considering Network Congestion by Probabilistic Model Checker PRISM2009

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Empirical Software Engineering in Practice 2009 (IWESEP2009)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] Qos Evaluation for Real-Time Distributed Systems Using the Probabilistic Model Checker Prism2009

    • 著者名/発表者名
      Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
    • 学会等名
      Proceedings of International Workshop on Informatics 2009 (IWIN2009)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] メソッドの自動生成を用いたOCLのJMLへの変換ツールの設計2009

    • 著者名/発表者名
      尾鷲方志, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
    • 発表場所
      (レクチャーノート・ソフトウェア学35ソフトウェア工学の基礎XVI)
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] フォーマルアプローチの基本技術習得のための学習支援システムの試作2009

    • 著者名/発表者名
      宮澤清介, 岡野浩三, 楠本真二
    • 学会等名
      情報処理学会ソフトウェア工学研究会ワークショップSES2009
    • 関連する報告書
      2013 研究成果報告書
  • [学会発表] メソッドの自動生成を用いたOCLのJMLへの変換ツールの設計2009

    • 著者名/発表者名
      尾鷲方志, 岡野浩三, 楠本真二
    • 学会等名
      日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
    • 発表場所
      箱根
    • 関連する報告書
      2009 実績報告書
  • [学会発表] Qos Evaluation for Real-Time Distributed Systems Using the Probabilistic Model Checker Prism2009

    • 著者名/発表者名
      長岡武志, 伊藤明彦, 岡野浩三, 楠本真二
    • 学会等名
      International Workshop on INformatics, IWIN 2009
    • 発表場所
      ハワイ, USA
    • 関連する報告書
      2009 実績報告書

URL: 

公開日: 2009-04-01   更新日: 2019-07-29  

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

Powered by NII kakenhi