Software Design using Model Cheking

• Project/Area Number: 21500036
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Osaka University
• Principal Investigator: OKANO Kozo 大阪大学, 情報科学研究科, 准教授 (70252632)
• Co-Investigator(Kenkyū-buntansha): 谷口 健一 (00029513)
• Project Period (FY): 2009-04-01 – 2014-03-31
• Project Status: Completed (Fiscal Year 2013)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2013: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2012: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000); Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: モデル検査 / モデル / 形式手法 / 時間オートマトン / CEGAR / OCL / JML / ソフトウェア / フォーマルアプローチ / モデル駆動開発 / 表明 / CEGAR LOOP / 確率時間オートマント

Research Abstract

This research investigates formal approach on software, especially design of software and its correctness.
The research mainly researches:
1 CEGAR loop algorithm for timed automaton; 2. JML-OCL conversion and its application to open softwares; 3. modelchecing of timed automata and its application to a line tracing robot; 4. JML assertion generation from ordinal program code using mathematical analysis on loop structure; and 5. automatic verification on consistency between equals method and hasCode method in Java programs.

Research Products

• [Journal Article] PDGとSMTソルバを利用した表明自動導出手法の提案と評価 (2013)
  • Author(s): 小林和貴, 佐々木幸広, 岡野浩三, 楠本真二
  • Journal Title: 電子情報通信学会論文誌 Volume: Vol.J96D, No.11(ソフトウェア基礎・応用特集号) Pages: 2657-2668
• [Journal Article] Alloy Analyzerを用いた表明に関する欠陥の検出手法—JMLによる表明記述に対して— (2013)
  • Author(s): 森恵弥佳, 岡野浩三, 楠本真二
  • Journal Title: 日本ソフトウェア科学会学会誌コンピュータソフトウェア Volume: Vol.30, No.3
  • NAID: 120005575505
• [Journal Article] Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model (2013)
  • Author(s): Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.5, No.3 Pages: 147-155
• [Journal Article] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml (2013)
  • Author(s): Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.5, No.2 Pages: 89-96
• [Journal Article] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml (2013)
  • Author(s): Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.5, No.2 Pages: 86-96
  • Peer Reviewed
• [Journal Article] Alloy Analyzer を用いた表明に関する欠陥の検出手 法―JML による表明記述に対して―” (2013)
  • Author(s): 森恵弥佳, 岡野浩三, 楠本真二
  • Journal Title: 日本ソフトウェア科学会学会誌コンピュータソフトウェア Volume: Vol.30, No.3,
  • NAID: 120005575505
  • Peer Reviewed
• [Journal Article] PDG とSMT ソルバを利用した表明自 動導出手法の提案と評価 (2013)
  • Author(s): 小林和貴, 佐々木幸広, 岡野浩三, 楠本真二
  • Journal Title: 電子情報通信学会論文誌 Volume: Vol.J96D, No.11 Pages: 2657-2668
  • Peer Reviewed
• [Journal Article] LASP - a Learning Assistant System for Formal Proof (2013)
  • Author(s): Kiyoyuki Miyazawa, Kozo Okano, and Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society (IJIS) Volume: vol.4, No.3
  • Peer Reviewed
• [Journal Article] Implementation of a Prototype Bi-directinal Translation Tool between Ocl and Jml (2013)
  • Author(s): Kentaro Hanada, Hiroaki Shinba, Kozo Okano, and Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society (IJIS) Volume: vol.5, No.1
  • Peer Reviewed
• [Journal Article] Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model (2013)
  • Author(s): Kozo Okano, Toshifusa Sekizawa, Hiroaki Shinba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society (IJIS) Volume: vol.5, No.1
  • Peer Reviewed
• [Journal Article] LASP—a Learning Assistant System for Formal Proof (2012)
  • Author(s): Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.4, No.2 Pages: 85-92
• [Journal Article] A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata (2011)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.3, No.1 Pages: 11-20
• [Journal Article] A Visualization Technique for Unit Testing and Static Checking with Caller-Callee Relationships (2011)
  • Author(s): Yuko Muto, Kozo Okano, Shinji Kusumoto
  • Journal Title: Journal of Convergences Volume: Vol.2, No. 2 Pages: 1-8
• [Journal Article] Daikon生成表明改善のためのテストケース自動生成手法とその評価実験 (2011)
  • Author(s): 宮本敬三, 堀直哉, 岡野浩三, 楠本真二
  • Journal Title: 日本ソフトウェア科学会学会誌コンピュータソフトウェア Volume: Vol. 28, No. 4
  • NAID: 130004549243
• [Journal Article] QoS Analysis of Real-time Distributed System Based on Hybrid Analysis of Probabilistic Model Checking (2011)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
  • Journal Title: IEICE Transactions on Information and Systems Volume: Vol.E94-D (フォーマルアプローチ特集号) Pages: 958-966
• [Journal Article] A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata (2011)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society (IJIS) Volume: Vol.3,No.1 Pages: 11-20
  • Peer Reviewed
• [Journal Article] An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop (2010)
  • Author(s): Takeshi Nagaoka, Kozo Okano, Shinji Kusumoto
  • Journal Title: IEICE Transactions on Information and Systems Volume: Vol.E93-D, No.5(フォーマルアプローチ特集号) Pages: 994-1005
  • NAID: 10026815323
• [Journal Article] メソッドの自動生成を用いたOCLのJMLへの変換 (2010)
  • Author(s): 尾鷲方志, 岡野浩三, 楠本真二
  • Journal Title: 日本ソフトウェア科学会学会誌コンピュータソフトウェア Volume: Vol. 27, No. 2
  • NAID: 130004549165
• [Journal Article] Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification (2009)
  • Author(s): Takeshi Nagaoka, Eigo Nagai, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society Volume: Vol.1, No.2 Pages: 37-44
• [Journal Article] Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification (2009)
  • Author(s): Takeshi Nagaoka, Eigo Nagai, Kozo Okano, Shinji Kusumoto
  • Journal Title: International Journal of Informatics Society (IJIS) Vol. 1, No. 2 Pages: 37-44
  • Peer Reviewed
• [Presentation] 形式手法ツール用のスクリプト言語について (2014)
  • Author(s): 岡野浩三
  • Organizer: ウィンターワークショッ プ2013・イン・大洗
  • Place of Presentation: 茨城 大洗
• [Presentation] Java におけるequals メソッドとhashCode メソッドの整合性の検査手法の提案 (2014)
  • Author(s): 榛葉浩章, 尾ノ上博樹, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術研究報告
  • Place of Presentation: 沖縄 那覇
• [Presentation] AC2Uppaal : A Tool for automatic Generation of Timed Automata for Analysis of Cyber-Physical Systems (2013)
  • Author(s): Emsaib Geepalla, Behzad Bordbar, Kozo Okano, Seyedhamed Seyedali
  • Organizer: the proceedings of the World Congress on Internet Security (WorldCIS-2013) IEEE
• [Presentation] Bidirectional Translation between OCL and JML for Round-trip Engineering (2013)
  • Author(s): Hiroaki Shimba, Kentaro Hanada, Kozo Okano, Shinji Kusumoto
  • Organizer: Accepted in the 5^<th> International Workshop on Empirical Software Engineering in Practice (IWESEP2013)
• [Presentation] Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects (2013)
  • Author(s): Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2013 (IWIN2013)
• [Presentation] A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC (2013)
  • Author(s): Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, Kozo Okano, Shinji Kusumoto, Kazuki Yoshioka
  • Organizer: Proceedings of International Workshop on Informatics 2013 (IWIN2013)
• [Presentation] Empirical Experiments on Software Assertion and Qualities (2013)
  • Author(s): Kozo Okano, Kazuki Yoshioka, Shinji Kusumoto
  • Organizer: Symposium on Advanced Information Systems (SAIS2013)
  • Place of Presentation: Copenhagen, Denmark
• [Presentation] AC2Uppaal: A Tool for automatic Generation of Timed Automata forAnalysis of Cyber-Physical Systems (2013)
  • Author(s): Emsaib Geepalla, Behzad Bordbar, Kozo Okano, and Seyedhamed Seyedali
  • Organizer: the World Congress on Internet Security 2013
  • Place of Presentation: London, UK
• [Presentation] Bidirectional Translation between OCL and JML for Round-trip Engineering (2013)
  • Author(s): Hiroaki Shimba, Kentaro Hanada, Kozo Okano, and Shinji Kusumoto
  • Organizer: International Workshop on Empirical Software Engineering in Practice 2013
  • Place of Presentation: Bankok, Thai
• [Presentation] Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects (2013)
  • Author(s): Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto
  • Organizer: International Workshop on Informatics 2013
  • Place of Presentation: Stockholm, Sweden
• [Presentation] Variable Coverage: A Metric to Evaluate the Exhaustiveness for Program Specifications Based on DbC (2013)
  • Author(s): Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, Kozo Okano, Shinji Kusumoto, and Kazuki Yoshioka
  • Organizer: International Workshop on Informatics 2013
  • Place of Presentation: Stockholm, Sweden
• [Presentation] Empirical Experiments on Software Assertion and Qualities (2013)
  • Author(s): Kozo Okano, Kazuki Yoshioka, and Shinji Kusumoto
  • Organizer: Symposium on Advanced Information Systems 2013
  • Place of Presentation: Copenhagen, Denmark
• [Presentation] SMT ソルバと統計解析を用いたJava プログラ ム解析器の提案 (2013)
  • Author(s): 佐々木幸広，岡野浩三，楠本真二
  • Organizer: 第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加 賀
  • Place of Presentation: 石川 加賀
• [Presentation] 制約記述言語OCL とJML の双方向変換手法の提 案 (2013)
  • Author(s): 榛葉浩章，岡野浩三，楠本真二
  • Organizer: 第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
  • Place of Presentation: 石川 加賀
• [Presentation] UML/OCL を用いたテスト自動生成手法のカバレッ ジ向上に関する一手法の提案 (2013)
  • Author(s): 藤田悠矢，岡野浩三，楠本真二
  • Organizer: 第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
  • Place of Presentation: 石川 加賀
• [Presentation] concolic execution を用いたバグ同定に関する研究 (2013)
  • Author(s): 大田崇史，岡野浩三，楠本真二
  • Organizer: 第20 回ソフトウェア工学の基礎ワークショップFOSE 2013 in 加賀
  • Place of Presentation: 石川 加賀
• [Presentation] 高位ソフトウェア設計検証をめざして (2013)
  • Author(s): 岡野浩三
  • Organizer: 高度情報シンポジウム2013
  • Place of Presentation: 北海道 知床
• [Presentation] PDG とSMT ソルバを用いたJava プログラム解析 器の提案 (2013)
  • Author(s): 佐々木幸広, 岡野浩三, 楠本真二
  • Organizer: SES2013 併設ワークショップ プログラム・デバッグ自動化の現状と今後
  • Place of Presentation: 東京
• [Presentation] ウィンターワークショップ2013・イン・那須報告 (2013)
  • Author(s): 野田夏子, 岡野浩三, 早水公二, 戸田航史, 上野秀剛, 石尾隆, 林晋平, 妻木俊彦, 中村匡 秀, 岸知二, 本橋正成, 鷲崎弘宜
  • Organizer: 情報処理学会研究報告
  • Place of Presentation: 東京
• [Presentation] 異なるスキーマ間に対応するSQL 文の整合性のAlloy Analyzer を用いた一検証手法 (2013)
  • Author(s): 藤田悠矢, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術研究報告
  • Place of Presentation: 北海道 札幌
• [Presentation] 契約記述の変更傾向の開発履歴情報を用いた調査 (2013)
  • Author(s): 吉岡一樹，岡野浩三，楠本真二:
  • Organizer: 電子情報通信学会技術報告, Vol.112, No.458, pp.121-126
  • Place of Presentation: 志賀島休暇村（福岡県）
• [Presentation] 在庫管理プログラムに対するAlloy Analyzer を用 いた検証事例 (2013)
  • Author(s): 森恵弥佳，岡野浩三，楠本真二
  • Organizer: ウィンターワークショップ2013・イン・那須
  • Place of Presentation: ラフォーレ那須(栃木県）
• [Presentation] 制約記述言語OCLとJMLのモデル駆動開発技法に基づいた双方向の変換手法の提案 (2012)
  • Author(s): 榛葉浩章, 花田健太郎, 岡野浩三
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 沖縄
  • Year and Date: 2012-03-13
• [Presentation] SMTソルバーとPDG作成ツールを用いたJavaのテストケース自動導出手法の提案 (2012)
  • Author(s): 佐々木幸広, 小林和貴, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 沖縄
  • Year and Date: 2012-03-13
• [Presentation] OCLからJMLへのDSLを用いた変換ツールの試作型の実装 (2012)
  • Author(s): 花田健太郎, 岡野浩三, 楠本真
  • Organizer: ウインターワークショップ2012・イン・琵琶湖
  • Place of Presentation: 長浜
  • Year and Date: 2012-01-20
• [Presentation] JMLによって記述された契約に対する品質評価手法の在庫管理プログラムへの適用 (2012)
  • Author(s): 吉岡一樹, 武藤祐子, 岡野浩三, 楠本真二
  • Organizer: ウインターワークショップ2012・イン・琵琶湖
  • Place of Presentation: 長浜
  • Year and Date: 2012-01-20
• [Presentation] 大学での形式手法の教育の一報告 (2012)
  • Author(s): 岡野浩三
  • Organizer: ウインターワークショップ2012・イン・琵琶湖
  • Place of Presentation: 長浜
  • Year and Date: 2012-01-20
• [Presentation] ライントレーサの定量的評価および検証に向けて (2012)
  • Author(s): 河井秀樹, 岡野浩三, 関潭俊弦
  • Organizer: ウインターワークショップ2012・イン・琵琶湖
  • Place of Presentation: 長浜
  • Year and Date: 2012-01-20
• [Presentation] Verification of Spatio-Temporal Role Based Access Control using Timed Automata,"In Proceedings of IEEE International Workshop on Design (2012)
  • Author(s): Emsaieb Geepalla, Behzad Bordbar, Kozo Okano
  • Organizer: Analysis and Tools for Integrated Circuits and Systems
• [Presentation] Verification of Safety Property of Line Tracer Program Using Timed Automaton Model (2012)
  • Author(s): Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2012 (IWIN2012)
• [Presentation] Implementation of a Prototype Bi-Directinal Translation Tool between Ocl and Jml (2012)
  • Author(s): Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2012 (IWIN2012)
• [Presentation] Practical Application of a Translation Tool from Uml/Ocl to Java Skeleton with Jml Annotation (2012)
  • Author(s): Kentaro Hanada, Kozo Okano, Shinji Kusumoto, Kiyoyuki Miyazawa
  • Organizer: Proceedings of 14th International Conference on Enterprise Information Systems (ICEIS2012)
• [Presentation] A Bi-directional Translation Tool between OCL and JML considering Reverse Translation (2012)
  • Author(s): Kentaro Hanada, Hiroaki Shimba, Kozo Okano, Shinji Kusumoto
  • Organizer: The 4th International Workshop on Empirical Software Engineering in Practice (IWESEP2012)
  • Place of Presentation: Osaka Japan (poster presentation)
• [Presentation] SMTを活用したJavaプログラム解析フレームワークの設計 (2012)
  • Author(s): 佐々木幸広, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第19回ワークショップFOSE2012
  • Place of Presentation: (レクチャーノート・ソフトウェア学38ソフトウェア工学の基礎XI)
• [Presentation] Practical Application of a Translation Tool from Uml/Ocl to Java Skeleton with Jml Annotation (2012)
  • Author(s): Kentaro Hanada, Kozo Okano, Shinji Kusumoto, and Kiyoyuki Miyazawa
  • Organizer: 14th International Conference on Enterprise Information Systems
  • Place of Presentation: Poland
• [Presentation] Implementation of a Prototype Bi-Directinal Translation Tool between Ocl and Jml, (2012)
  • Author(s): Kentaro Hanada, Hiroaki Shinba, Kozo Okano, and Shinji Kusumoto
  • Organizer: International Workshop on Informatics 2012
  • Place of Presentation: France
• [Presentation] Verification of Safety Property of Line Tracer Program Using Timed Automaton Model (2012)
  • Author(s): Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto
  • Organizer: International Workshop on Informatics 2012
  • Place of Presentation: France
• [Presentation] A Bi-directional Translation Tool between OCL and JML considering Reverse Translation (2012)
  • Author(s): Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto
  • Organizer: The 4th InternationalWorkshop on Empirical Software Engineering in Practice (IWESEP2012)
  • Place of Presentation: 大阪大学（大阪府）
• [Presentation] SMT を活用したJava プログラム解析フレーム ワークの設計 (2012)
  • Author(s): 佐々木幸広，岡野浩三，楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16 回 8 ワークショップFOSE2012
  • Place of Presentation: ゆふいん山水館(大分県）
• [Presentation] UPPAAL によるライント レーサの安全性検証のケーススタディ (2012)
  • Author(s): 岡野浩三，関澤俊弦，花田健太郎，榛葉浩章，楠本真二:
  • Organizer: SES2012 併設ワークショップ (WS-4) 形式 手法の今と未来
  • Place of Presentation: 東京電機大学（東京都）
• [Presentation] OCL との比較を用いた形式仕様記述言語JML の 品質評価メトリクスの提案 (2012)
  • Author(s): 吉岡一樹，岡野浩三，楠本真二
  • Organizer: SES2012 併設ワークショップ (WS-4) 形式 手法の今と未来
  • Place of Presentation: 東京電機大学（東京都）
• [Presentation] ウィンター ワークショップ2012・イン・琵琶湖開催報告 (2012)
  • Author(s): 丸山勝久，大森隆行，井垣宏，中村匡秀，伏田享平，角田雅照，風戸広史，岡田譲二， 岡野浩三，坂本一憲，本橋正成，岸知二，野田夏子，小林隆志，林晋平
  • Organizer: 情報処理学会研究報告, Vol.2012-SE-178, No.11
  • Place of Presentation: 琵琶湖コンファレンスセンター（滋賀県）
• [Presentation] Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton (2011)
  • Author(s): Kozo Okano, Behzad Bordbar, Takeshi Nagaoka
  • Organizer: 2nd International Conference on Networking and Computing
  • Place of Presentation: Osaka
  • Year and Date: 2011-12-02
• [Presentation] 呼び出し関係を用いた単体テストおよび静的検査の可視化手法の改善とその評価 (2011)
  • Author(s): 武藤祐子, 岡野浩三, 楠本真二
  • Organizer: 「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2011
  • Place of Presentation: 青森
  • Year and Date: 2011-11-25
• [Presentation] Improvement of a Visualization Technique for the Passage Rate of Unit Testing and Static Checking and its Evaluation (2011)
  • Author(s): Yuko Mutoh, Kozo Okano, Shinji Kusumoto
  • Organizer: The Joint Conference of the 21th International Workshop on Software Measurement (IWSM) and the 6th International Conference on Software Process and Product Measurement (Mensura)
  • Place of Presentation: Nara
  • Year and Date: 2011-11-03
• [Presentation] JMLによって記述された契約に対する品質評価手法の提案 (2011)
  • Author(s): 武藤祐子, 岡野浩三, 楠本真二
  • Organizer: 平成23年度情報処理学会関西支部支部大会
  • Place of Presentation: 大阪
  • Year and Date: 2011-09-22
• [Presentation] Daikonを利用した表明動的生成改善手法の実プロジェクト教材への適用実験とテストデータ生成改善手法の検討 (2011)
  • Author(s): 小林和貴, 岡野浩三, 楠本真二
  • Organizer: 平成23年度情報処理学会関西支部支部大会
  • Place of Presentation: 大阪
  • Year and Date: 2011-09-22
• [Presentation] LASP-a Learning Assistant System for Formal Proof (2011)
  • Author(s): Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
  • Organizer: International Workshop on INformatics, IWIN 2011
  • Place of Presentation: Venice
  • Year and Date: 2011-09-20
• [Presentation] モデル検査器とDaikonを用いた表明動的生成改善手法のシステム開発実プロジェクト教材への適用と評価 (2011)
  • Author(s): 小林和貴, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 札幌
  • Year and Date: 2011-07-30
• [Presentation] A Visualization Technique for the Passage Rate of Unit Testing and Static Checking with Caller-Callee Relationships (2011)
  • Author(s): Yuko Mutoh, Kozo Okano, Shinji Kusumoto
  • Organizer: International Conference on Advanced Software Engineering 2011
  • Place of Presentation: Pusan
  • Year and Date: 2011-05-27
• [Presentation] 複数反例抽出を用いたCEGARによる時間オートマトンの抽象洗練手法 (2011)
  • Author(s): 田中俊彰, 長岡武志, 岡野浩三, 楠本真二
  • Organizer: 情報処理学会研究報告
  • Place of Presentation: 東京
  • Year and Date: 2011-03-15
• [Presentation] OCLからJMLへの変換ツールにおける対応クラスの拡張と教務システムに対する適用実験 (2011)
  • Author(s): 宮澤清介, 花田健太郎, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 沖縄
  • Year and Date: 2011-03-08
• [Presentation] Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton (2011)
  • Author(s): Kozo Okano, Behzad Bordbar, Takeshi Nagaoka
  • Organizer: proceedings of the 2nd International Conference on Networking and Computing
• [Presentation] LASP - a Learning Assistant System for Formal Proof (2011)
  • Author(s): Kiyoyuki Miyazawa, Kozo Okano, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2011 (IWIN2011)
• [Presentation] Improvement of a Visualization Technique for the Passage Rate of Unit Testing and Static Checking and its Evaluation (2011)
  • Author(s): Yuko Muto, Kozo Okano, Shinji Kusumoto
  • Organizer: 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)
• [Presentation] A Visualization Technique for the Passage Rate of Unit Testing and Static Checking with Caller-Callee Relationships (2011)
  • Author(s): Yuko Muto, Kozo Okano, Shinji Kusumoto
  • Organizer: International Conference on Advanced Software Engineering 2011
• [Presentation] 呼び出し関係を用いた単体テストおよび静的検査の可視化手法の改善とその評価 (2011)
  • Author(s): 武藤祐子, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第18回ワークショップFOSE2011
  • Place of Presentation: (レクチャーノート・ソフトウェア学37ソフトウェア工学の基礎XVIII)
• [Presentation] アサーション動的生成を目的としたテストケース制約のESC/Java2を利用した導出 (2011)
  • Author(s): 小林和貴, 宮本敬三, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第17回ワークショップFOSE2010
  • Place of Presentation: (レクチャーノート・ソフトウェア学36ソフトウェア工学の基礎VII)
• [Presentation] アサーション動的生成を目的としたテストケース制約のESC/Java2を利用した導出 (2010)
  • Author(s): 小林和貴, 宮本敬三, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2010
  • Place of Presentation: 新潟
  • Year and Date: 2010-11-19
• [Presentation] 時間システムの到達可能性解析の並列手法と評価実験 (2010)
  • Author(s): 田中俊彰, 長岡武志, 岡野浩三, 楠本真二
  • Organizer: 情報処理学会研究報告
  • Place of Presentation: 大阪大学
  • Year and Date: 2010-11-12
• [Presentation] OCLのJMLへの変換ツールの実装と評価 (2010)
  • Author(s): 宮澤清介, 岡野浩三, 楠本真二
  • Organizer: 情報処理学会研究報告
  • Place of Presentation: 大阪大学
  • Year and Date: 2010-11-12
• [Presentation] 時間システムの到達可能性解析の並列手法と評価実験 (2010)
  • Author(s): 田中俊彰, 長岡武志, 岡野浩三, 楠本真二
  • Organizer: 平成22年度情報処理学会関西支部支部大会
  • Place of Presentation: 大阪
  • Year and Date: 2010-09-22
• [Presentation] 数理論理学の形式証明に対する学習支援システムの試作と評価 (2010)
  • Author(s): 宮澤清介, 岡野浩三, 楠本真二
  • Organizer: 平成22年度情報処理学会関西支部支部大会
  • Place of Presentation: 大阪
  • Year and Date: 2010-09-22
• [Presentation] Reachability Analysis of Probabilistic Real-Time Systems Based on CEGAR for Timed Automata (2010)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
  • Organizer: International Workshop on INformatics, IWIN 2010
  • Place of Presentation: エジンバラ英国
  • Year and Date: 2010-09-13
• [Presentation] クラス間関係を利用した単体テストおよび静的検査の網羅率可視化手法 (2010)
  • Author(s): 武藤祐子, 岡野浩三, 楠本真二
  • Organizer: 情報処理学会ソフトウェア工学研究会ワークショップSES2010
  • Place of Presentation: 東洋大
  • Year and Date: 2010-09-01
• [Presentation] OCLのJMLへの変換ツールの実装 (2010)
  • Author(s): 宮澤清介, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 北海道大学
  • Year and Date: 2010-08-06
• [Presentation] 実時間システムを対象としたCEGARによる抽象洗練の並列化手法 (2010)
  • Author(s): 田中俊彰, 長岡武志, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 北海道大学
  • Year and Date: 2010-08-05
• [Presentation] 時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析 (2010)
  • Author(s): 伊藤明彦, 長岡武志, 岡野浩三, 楠本真二
  • Organizer: 電子情報通信学会技術報告
  • Place of Presentation: 鹿児島
  • Year and Date: 2010-03-08
• [Presentation] Reachability Analysis of Probabilistic Timed Automata Based on an Abstraction Refinement Technique (2010)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, Shinji Kusumoto
  • Organizer: International Workshop on Empirical Software Engineering in Practice 2010
• [Presentation] Reachability Analysis of Probabilistic Real-Time Systems Based on CEGAR for Timed Automata (2010)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2010 (IWIN2010)
• [Presentation] クラス間関係を利用した単体テストおよび静的検査の網羅率可視化手法 (2010)
  • Author(s): 武藤祐子, 岡野浩三, 楠本真二:
  • Organizer: 情報処理学会ソフトウェア工学研究会ワークショップSES2010,ソフトウェアエンジニアリング最前線2010
• [Presentation] アサーション動的生成のためのテストケース自動生成手法の生成アサーションの妥当性評価 (2010)
  • Author(s): 宮本敬三, 堀直哉, 岡野浩三, 楠本真二, 西本哲
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
  • Place of Presentation: (レクチャーノート・ソフトウェア学35ソフトウェア工学の基礎XVI)
• [Presentation] Qualitative Analysis of Real-time Distributed Systems Considering Network Congestion by Probabilistic Model Checker PRISM (2009)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Empirical Software Engineering in Practice 2009 (IWESEP2009)
• [Presentation] Qos Evaluation for Real-Time Distributed Systems Using the Probabilistic Model Checker Prism (2009)
  • Author(s): Takeshi Nagaoka, Akihiko Ito, Kozo Okano, Shinji Kusumoto
  • Organizer: Proceedings of International Workshop on Informatics 2009 (IWIN2009)
• [Presentation] メソッドの自動生成を用いたOCLのJMLへの変換ツールの設計 (2009)
  • Author(s): 尾鷲方志, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
  • Place of Presentation: (レクチャーノート・ソフトウェア学35ソフトウェア工学の基礎XVI)
• [Presentation] フォーマルアプローチの基本技術習得のための学習支援システムの試作 (2009)
  • Author(s): 宮澤清介, 岡野浩三, 楠本真二
  • Organizer: 情報処理学会ソフトウェア工学研究会ワークショップSES2009
• [Presentation] メソッドの自動生成を用いたOCLのJMLへの変換ツールの設計 (2009)
  • Author(s): 尾鷲方志, 岡野浩三, 楠本真二
  • Organizer: 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16回ワークショップFOSE2009
  • Place of Presentation: 箱根
• [Presentation] Qos Evaluation for Real-Time Distributed Systems Using the Probabilistic Model Checker Prism (2009)
  • Author(s): 長岡武志, 伊藤明彦, 岡野浩三, 楠本真二
  • Organizer: International Workshop on INformatics, IWIN 2009
  • Place of Presentation: ハワイ, USA