信州大学HOMEENGLISH交通・キャンパス案内

研究者総覧研究者総覧

研究者、研究内容などで検索
項目別検索はこちら

岡野浩三  オカノ コウゾウ

教員組織学術研究院(工学系)電話番号
教育組織工学部 電子情報システム工学科FAX番号
職名准教授メールアドレスokano@cs.shinshu-u.ac.jp
住所〒380-8553 長野県長野市若里4-17-1ホームページURLhttp://softeng-www.cs.shinshu-u.ac.jp

プロフィール

研究分野
ソフトウェア工学
現在の研究課題
モデル検査を用いた要求仕様検証
キーワード:仕様記述 , モデル検査 , 形式技法
所属学会
所属学会
情報処理学会
電子情報通信学会
日本ソフトウェア科学会
IEEE
学歴
出身大学院
1993 , 大阪大学 , 大学院基礎工学研究科 , 物理系専攻 情報工学分野
1992 , 大阪大学 , 大学院基礎工学研究科 , 物理系専攻 情報工学分野

出身学校・専攻等(大学院を除く)
1990 , 大阪大学 , 基礎工学部 , 情報工学科

取得学位
博士(工学) , 大阪大学
受賞学術賞
2015 , IPA/SEC 論文賞2014年度SEC所長賞
2008 , 情報処理学会組み込みシステムシンポジウム奨励賞
1997 , 情報処理学会大会優秀賞
研究職歴等
研究職歴
2015- , 信州大学工学部准教授
2011-2012 , 大阪大学教育実践センター准教授(兼任)
2007-2015 , 大阪大学大学院情報科学研究科准教授(職名改正)
2007-2007 , 大阪府立大学理学部 非常勤講師
2002-2007 , 大阪大学大学院情報科学研究科助教授
1999-2002 , 大阪大学大学院基礎工学研究科講師
1997-1999 , 大阪大学大学院基礎工学研究科助手(大学院重点化)
1993-1997 , 大阪大学基礎工部助手

研究活動業績

研究業績(著書・
発表論文等)
著書
アサーションベース設計
丸善 , :- 2004
Author:Harry D. Foster, Adam C. Krolnik, David J. Lacey著 後藤謙治 [ほか] 訳


論文
On the Generation of Human-oriented Counter-examples using a Test Automaton,
International Journal of Informatics Society,9(1):pp.41-50 2017(Jun. 01)
Author:Chikyu Yanagisawa, Shinpei Ogata, Kozo Okano


Parallel Multiple Counter-Examples Guided Abstraction Loop –Applying to Timed Automaton–
International Journal of Informatics Society,8(2):pp.103-116 2016(Apr. 01)
Author:Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, Shinji Kusumoto


ソフトウェア文書匿名化ツールの試作
電子情報通信学会論文誌,J98D(11):pp.1419-1422 2015(Nov. 01)
Author:江川翔太, 岡野浩三, 楠本真二


Formal Verification Technique for Consistency Checking between equals and hashCode Methods in Java
International Journal of Informatics Society,7(2):pp.77-87 2015(Aug. 01)
Author:Kozo Okano, Hiroaki Shimba, Takafujmi Ohta, Hiroki Onoue, and Shinji Kusumoto


ソースコードからのプラットフォーム依存部抽出手法
SEC Journal,10(5):8-17 2015(Jan.)
Author:岡本周之 , 藤原貴之, 岡野浩三, 楠本真二


New Metrics for Program Specifications Based on DbC
International Journal of Informatics Society,6(2):79-87 2014
Author:Kozo Okano, Yuko Muto, Yukihiro Sasaki, Takafumi Ohta, and Shinji Kusumoto


Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects
International Journal of Informatics Society,6(2):79-87 2014
Author:Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto


PDGとSMTソルバを利用した表明自動導出手法の提案と評価(ソフトウェア工学,<特集>ソフトウェア基礎・応用論文)
電子情報通信学会論文誌. D, 情報・システム,96(11):2657-2668 2013(Nov.)
Author:小林和貴, 佐々木幸広, 岡野浩三, 楠本真二


Implementation of a Prototype Bi-directional Translation Tool between Ocl and Jml
International Journal of Informatics Society,5(2):89-96 2013
Author:Kentaro Hanada, Hiroaki Shimba, Kozo Okano, and Shinji Kusumoto


Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model
International Journal of Informatics Society,5(3):147-155 2013
Author:Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto


Alloy Analyzerを用いた表明に関する欠陥の検出手法 —JMLによる表明記述に対して—
コンピュータ ソフトウェア,30(3):3_187-3_193 2013
Author:森恵弥佳, 岡野浩三, 楠本真二


LASP --- a Learning Assistant System for Formal Proof
International Journal of Informatics Society,4(2):85-92 2012
Author:Kiyoyuki Miyazawa, Kozo Okano, and Shinji Kusumoto


QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS,E94D(5):958-966 2011(May)
Author:Takeshi Nagaoka,, Akihiko Ito, KozoOkano, and Shinji Kusumoto


A Visualization TEchnique for Unit Testing and Static Checking with Caller-Callee Relationships
Journal of Convergences,2(2):1-8 2011(Feb.)
Author:Yuko Muto, Kozo Okano, and Shinji Kusumoto


A Model Abstraction Technique for Probabilistic Real-Time Systems Based on CEGAR for Timed Automata
International Journal of Informatics Society,3(1):11-20 2011
Author:Takeshi Nagaoka, Akihiko Ito, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto


Daikon生成表明改善のためのテストケース自動生成手法とその評価実験
コンピュータ ソフトウェア,28(4):306-317 2011
Author:宮本敬三, 堀直哉, 岡野浩三, 楠本真二


An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS,E93D(5):994-1005 2010(May)
Author:Takeshi Nagaoka, Kozo Okano, and Shinji Kusumoto


メソッドの自動生成を用いたOCLのJMLへの変換
コンピュータ ソフトウェア,27(2):106-111 2010
Author:尾鷲方志, 岡野浩三, 楠本真二


Stepwise Approach to Design of Real-Time Systems based UML/OCL with Formal Verification
International Journal of Informatics Society,1(2):33-44 2009
Author:Takeshi Nagaoka, Eigo Nagai, Toshiaki Tanaka, Kozo Okano, and Shinji Kusumoto


在庫管理プログラムの設計に対するJML記述とESC/Java2を用いた検証の事例報告(研究速報)
電子情報通信学会論文誌. D, 情報・システム,91(11):2719-2720 2008(Nov. 01)
Author:尾鷲方志, 岡野浩三, 楠本真二


Javaに対するループインバリアントを含むDaikon生成アサーションの妥当性評価(研究速報)
電子情報通信学会論文誌. D, 情報・システム,91(11):2721-2723 2008(Nov. 01)
Author:宮本敬三, 岡野浩三, 楠本真二


上位設計におけるシステムの振る舞い検証技術
システム制御情報学会誌,52(9):328-333 2008(Sep. 15)
Author:岡野浩三


制約指向に基づいたUMLモデルの不整合検出・解消手法の提案(ソフトウェア,<特集>フォーマルアプローチ論文)
電子情報通信学会論文誌. D, 情報・システム,90(4):1005-1013 2007(Apr. 01)
Author:佐々木亨, 岡野浩三, 楠本真二


時間制約を保証するUML/OCLを用いた分散実時間アプリケーション開発手法(ソフトウェア,<特集>フォーマルアプローチ論文)
電子情報通信学会論文誌. D, 情報・システム,89(4):683-692 2006(Apr. 01)
Author:長井栄吾, 牧寺彩, 岡野浩三, 谷口健一


A Timed Automata Approach to QoS Resolution
International Journal of Simulation Systems, Science & Technology Special Issue on: Performance Evaluation of Computer Systems,7(1):46-54 2006
Author:Behzad Bordbar, Rachid Anane, and Kozo Okano


外部入力値のみを保持できる整数変数をもつFSMに対する記号モデル検査法(ソフトウェア工学)
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理,87(4):462-470 2004(Apr. 01)
Author:竹中崇, 岡野浩三, 東野輝夫, 谷口健一


凹多面体併合を用いた有理数プレスブルガー文真偽判定アルゴリズムの実装と形式的設計検証への適用
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理,84(7):999-1008 2001(Jul. 01)
Author:柴田直樹, 岡野浩三, 谷口健一


CPU設計導入教育への形式的設計検証手法の適用
情報処理学会論文誌,41(11):3114-3121 2000(Nov. 15)
Author:北浜優子, 北嶋暁, 岡野浩三, 谷口健一


冠頭標準形有理数プレスブルガー文の真偽判定アルゴリズムの提案
電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理,82(6):691-700 1999(Jun. 25)
Author:柴田直樹, 岡野浩三, 東野輝夫, 谷口健一


遷移の選択が状態訪問回数で決まる有限状態機械対からなる通信系に対する生存性の検証
情報処理学会論文誌,39(3):750-759 1998(Mar. 15)
Author:水野健太郎, 中田明夫, 岡野浩三, 東野輝夫, 谷口健一


時間ペトリネットの拡張モデルを用いたプロトコル合成
情報処理学会論文誌,39(3):769-778 1998(Mar. 15)
Author:山口弘純, 岡野浩三, 東野輝夫, 谷口健一


共有メモリ型並列計算機上での正則な項書換え系の一実装法
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ,81(1):28-37 1998(Jan. 25)
Author:松石航也, 服部哲, 岡野浩三, 東野輝夫, 谷口健一


レジスタ付きペトリネットを用いた全体動作仕様から分散動作仕様の自動合成とその応用 (<小特集>コンカレント・コラボレーション技術論文小特集)
電子情報通信学会論文誌. A, 基礎・境界,80(7):1064-1072 1997(Jul. 25)
Author:山口弘純, 岡野浩三, 東野輝夫, 谷口健一


あるスタイルに基づく順序機械型記述における詳細化の正しさの証明方法
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ,78(7):622-633 1995(Jul. 25)
Author:岡野浩三, 東野輝夫, 谷口健一


グル-プワ-クを考慮した協調計算システムにおける動作プログラム群の生成と分散実行
情報処理学会論文誌,36(6):1367-1378 1995(Jun. 15)
Author:伊東達雄, 今城広志, 岡野浩三, 東野輝夫, 松浦敏雄, 谷口健一


関係デ-タベ-スを用いた在庫管理プログラムの記述とその詳細化の正しさの証明
情報処理学会論文誌,36(5):1091-1103 1995(May 15)
Author:森岡 澄夫; 岡野 浩三; 東野 輝夫; 谷口 健一;


リンクの故障を考慮に入れた分散システムの動作仕様の自動導出
情報処理学会論文誌,36(1):70-83 1995(Jan. 15)
Author:岡野浩三, 今城広志, 東野輝夫, 谷口健一


Synthesis of Protocol Specifications from Service Specifications of Distributed Systems in a Marked Graph Model
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTONICS, COMMUNICATIONS AND COMPUTER SCIENCES,E77-A(10):1623-1633 1994
Author:Hirozumi Yamaguchi, Kozo Okano, Teruo Higashino, and Kenichi Taniguchi


順序機械型プログラムの階層的設計法と在庫管理プログラムの開発例
電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ,76(7):354-363 1993(Jul. 25)
Author:岡野浩三, 北道淳司, 東野輝夫, 谷口健一


拡張有限状態機械モデルを用いた分散システムの要求仕様から各ノードの動作仕様の自動導出
情報処理学会論文誌,34(6):1290-1301 1993(Jun. 15)
Author:岡野浩三, 今城広志, 東野輝夫, 谷口健一


学会発表
Equivalence Checking of Java Methods — Toward Ensuring IoT Dependability —
Proceedings of The 26th International Conference on Computer Communications and Networks (ICCCN 2017) 2017(Aug. 01)
Author:Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, Shin Nakajima


A Method for Removing Ambiguity in Designing Sequence Diagrams for Developing Communication Programs
Proceedings of International Workshop on Informatics 2016 , 2016:pp.243-248 2016(Sep. 01)
Author:Kozo Okano, Satoshi Harauchi, Kozo Okano, Shinpei Ogata


Framework for Relative Web Usability Evaluation on Usability Features in MDD
LNCS , 9856:pp.73-85 2016(Aug. 01)
Author:Shinpei Ogata, Yugo Goto, Kozo Okano


Behavior Verification of Autonomous Robot Vehicle in Consideration of Errors and Disturbances
IEEE , Computer Software and Applications Conference (COMPSAC) , 3:550-555 2015(Jul.)
Author:Toshifusa Sekizawa, Fumiya Otsuki, Kazuki Ito, and Kozo Okano


画面遷移モデルに基づくシナリオ作成支援手法の検討 (知能ソフトウェア工学)
電子情報通信学会 , 電子情報通信学会技術研究報告 , 115(54):7-12 2015(May 25)
Author:小形真平, 中村哲真, 岡野浩三


Safety Verification of Multiple Autonomous Systems by Formal Approach
LNCS , 8696:11-18 2014(Sep.)
Author:Kozo Okano and Toshifusa Sekizawa


Verification of Spatio-Temporal Role Based Access Control using Timed Automata
Proceedings of IEEE International Workshop on Design, Analysis and Tools for Integrated Circuits and Systems , :1-6 2012
Author:Emsaieb Geepalla, Behzad Bordbar, and Kozo Okano


Clock Number Reduction Abstraction on CEGAR Loop Approach to Timed Automaton
Prpoceedings of the 2nd International Conference on Networking and Computing , :235-242 2011
Author:Kozo Okano, Behzad Bordbar, and Takeshi Nagaoka


A Method to Generate Pre- and Postconditions for Java Methods Based on Hybrid Analysis
Proceedings of International Workshop on Informatics 2008 , :82-89 2008
Author:Kozo Okano, Shinji Kusumoto, and Yasunobu Kajita


An Evaluation Mechanism for QoS Management in Wireless Systems
Proceedings of ICPADS 2005 , II:150-154 2005
Author:Behzad Bordbar, Rachid Anane, and Kozo Okano


Testing Deadlock-freeness in Real-time Systems --- A Formal Approach ---
LNCS , 3395:95-109 2004
Author:Behzad Bordbar and Kozo Okano


Verification of Timeliness QoS Properties in Multimedia Systems
LNCS , 2885:532-540 2003
Author:Behzad Bordbar and Kozo Okano


その他
Special Section on Formal Approach FOREWORD
IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS , E98D(6):1120-1120 2015(Jun.)
Author: Kozo Okano

研究費
共同研究
2016 - 2017 , 国内共同研究

受託研究
2017 - 2017 , ソフトウェア設計に関する共同研究 三菱電機(株)
2016 - 2016 , ソフトウェア設計に関する共同研究 三菱電機(株)
2015 - 2015 , ソフトウェア設計に関する共同研究 三菱電機(株)

科学研究費補助金(研究代表者)
2016 - 2018 , モデルと制約に基づくソフトウェア開発に関する研究
研究諸活動
在外研究員等
2002-2003 , 文部科学省在外研究 , 英国Kent大学、英国 Birmingham大学

その他研究活動
2016-2016 , 国際会議International Workshop on Informatics IWIN General Co-Chair
2015-2015 , 電子情報通信学会和文論文誌D ソフトウェア基礎・応用特集号 編集委員会幹事
2015-2015 , 国際会議 Asia-Pacific Software Engineering Conference APSEC PC委員
2015-2015 , 情報処理学会組込みシステム研究会シンポジウム ESS実行副委員長
2014-2015 , 電子情報通信学会英文D 誌フォーマルアプローチ特集号 編集委員会委員長
2014-2014 , 情報処理学会組込みシステム研究会シンポジウム PC委員長
2014-2014 , 国際会議International Workshop on Informatics IWIN General Co-Chair
2013-2013 , 電子情報通信学会和文論文誌D ソフトウェア基礎・応用特集号 編集委員会幹事
2013-2013 , 情報処理学会組込みシステム研究会シンポジウム ESS 共同PC副委員長
2013-2013 , 日本ソフトウェア科学会ソフトウェア工学の基礎研究会ワークショップFOSE 共同PC委員長
2013-2013 , 日本ソフトウェア科学会 ソフトウェア工学特集号 編集委員
2012-2013 , 電子情報通信学会和文論文誌D システム論文特集号編集委員会委員
2012-2014 , 電子情報通信学会英文D 誌フォーマルアプローチ特集号編集委員会幹事
2012-2013 , 国際会議International Workshop on Informatics IWIN PC Chair
2011-2015 , 電子情報通信学会和文論文誌D 学生論文特集号編集委員会委員
2011-2015 , 電子情報通信学会和文論文誌D 編集委員会委員
2011-2015 , 情報処理学会論文誌ジャーナル/JIP 論文誌編集委員会委員
2011-2013 , 情報処理学会ソフトウェア工学特集号編集委員
2011-2013 , 電子情報通信学会英文D 誌フォーマルアプローチ特集号編集委会委員
2009-2010 , 国際会議Australasian Software Engineering Conference ASWEC PC委員
2009-2009 , 国際会議Adaptive Systems in Heterogeneous Environments ASHEs PC委員
2009-2009 , 国際会議Asia-Pacific Software Engineering Conference APSEC PC委員
2008-2012 , 情報処理学会ソフトウェア工学研究会運営委員
2008-2008 , 国際会議Asia-Pacific Software Engineering Conference APSEC PC委員
2007-2012 , 情報処理学会組込みシステム研究会シンポジウム ESS PC委員
2007-2012 , 日本ソフトウェア科学会ソフトウェア工学の基礎研究会ワークショップ FOSE PC委員
2005-2005 , 日本ソフトウェア科学会プログラミングおよびプログラミング言語ワークショップPPL PC委員
2004-2004 , ソフトウェアシンポジウムPC委員
2004-2004 , LA シンポジウム事務局庶務
2002-2011 , 電子情報通信学会ソフトウェアサイエンス研究会専門委員