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

研究者総覧研究者総覧

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

岡野 浩三  オカノ コウゾウ

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

プロフィール

研究分野
ソフトウェア工学
キーワード:仕様記述 , 検証
現在の研究課題
モデル検査を用いた要求仕様検証
キーワード:仕様記述 , モデル検査 , 形式技法
モテルと制約に基つくソフトウェア開発に関する研究
20160400-20190300
モデル検査技術を活用したソフトウェア設計方法に関する研究
20090400-20140300
状態爆発するWEB アプリケーションに対するソフトウェアモデル検査
20060400-20070300
契約に基づいた関数型プログラム設計に対する正当性保証に関する研究
20050400-20070300
関数型プログラムに対するモジュール構造を考慮に入れた効率のよい形式的検証支援
20020400-20050300
所属学会
所属学会
情報処理学会
電子情報通信学会
日本ソフトウェア科学会
IEEE

所属学会役職担当
2022-2024 , 電子情報通信学会 , ソフトウェアサイエンス研究会専門委員長
2020-2022 , 電子情報通信学会 , ソフトウェアサイエンス研究会専門副委員長
学歴
出身大学院
1995 , 大阪大学 , 大学院基礎工学研究科 , 物理系専攻 情報工学分野 (論文博士)
1993 , 大阪大学 , 大学院基礎工学研究科 , 物理系専攻 情報工学分野 (文部教官助手採用のため退学)
1992 , 大阪大学 , 大学院基礎工学研究科 , 物理系専攻 情報工学分野 (修了)

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

取得学位
博士(工学) , 大阪大学
修士(工学) , 大阪大学
受賞学術賞
2017 , International Workshop on Informatics, Excellent Paper Award
2016 , 電子情報通信学会 情報・システムソサエティ 活動功労賞
2015 , 電子情報通信学会 情報・システムソサエティ論文編集活動感謝状
2015 , IPA/SEC 論文賞2014年度SEC所長賞
2010 , International Workshop on Informatics. Bet Paper Award
2008 , 情報処理学会組み込みシステムシンポジウム奨励賞
1997 , 情報処理学会大会優秀賞
研究職歴等
研究職歴
2020- , 信州大学工学部教授
2015-2020 , 信州大学工学部准教授
2011-2012 , 大阪大学教育実践センター准教授(兼任)
2007-2015 , 大阪大学大学院情報科学研究科准教授(職名改正)
2007-2007 , 大阪府立大学理学部 非常勤講師
2002-2007 , 大阪大学大学院情報科学研究科助教授
1999-2002 , 大阪大学大学院基礎工学研究科講師
1997-1999 , 大阪大学大学院基礎工学研究科助手(大学院重点化)
1993-1997 , 大阪大学基礎工部助手

研究活動業績

研究業績(著書・
発表論文等)
書籍等出版物
システム技術に基づく安全設計ガイド
電波新聞社 2019
Author:兼本 茂 , 余宮 尚志, 入月 康晴, 長久保 隆一, 三原 幸博, 岡本 圭史, 岡野 浩三


アサーションベース設計, -
丸善 2004
Author:Harry D. Foster, Adam C. Krolnik, David J. Lacey著 後藤謙治 [ほか] 訳


論文
Proposal and Evaluation for A Method to Verify Equivalence of Specifications of C and Java Functions with Recursive Data Structures by SAW: Case Studies of Linear Structures and Binary Trees
International Journal of Informatics Society,12(3):pp.143-156 2021(Mar.)
Author:Rin Karashima, Kozo Okano, Shinpei Ogata, Satoshi Harauchi, and Toshifusa Sekizawa


Regression Verification for C Functions with Recursive Data Structure
,11(2):pp.107-115 2019(Oct.)
Author:Kozo Okano, Rin Karashima, Satoshi Harauchi, and Shinpei Ogata


Consistency Checking between Java Equals and hashCode Methods Using Software Analysis Workbench
IEICE Transactions on Information and Systems,E102(8):pp.1419-1422 2019(Aug.)
Author:Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, and Shin Nakajima


Effective Derivation of a Mapping of Variables in a Loop Structure
International Journal of Informatics Society,10(2):pp.75-83 2018(Sep.)
Author:Kozo Okano, Shinji Kusumoto, and Yukihiro Sasaki


Support Tool for Refining Conceptual Model in Collaborative Learning
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering,:pp.168-167 2018(Aug.)
Author:Misaki Maruyama, Shinpei Ogata, Kozo Okano, and Mizue Kayama


Analysis of Specification in Japanese using Natural Language Processing
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering,:pp.12-21 2018(Aug.)
Author:Kozo Okano, Kazuma Takahashi, Shinpei Ogata, and Toshifusa Sekizawa


STAMP海外事例の紹介: STPA-SafeSec
SEC journal,13(4):pp.42-47 2018(Apr.)
Author:岡本圭史, 岡野浩三


Removing Ambiguous Message Exchanges in Designing Sequence
International Journal of Informatics Society,9(3):pp.129-138 2017(Dec.)
Author:Satoshi Harauchi, Kozo Okano, and Shinpei Ogata


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


契約を用いたソフトウェア開発の修正傾向調査
SEC Journal,11(3):pp.8-15 2016(Jan. 01)
Author:岡野浩三, 吉岡一樹, 楠本真二


ソフトウェア文書匿名化ツールの試作
電子情報通信学会論文誌,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, 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:Tekeshi Nagaoka, Kozo Okano, and, Shinji Kusumoto


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:岡野浩三, 今城広志, 東野輝夫, 谷口健一


講演・口頭発表等
Edutainment を指向したソフトウェア教育用フレームワークの提案
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020 2020(Dec.)
Presenter:堤 崚介, 魏 久竣, 岡野浩三, 小形真平, 新村正明


モデル検査における複雑な検査式に対する反例解析手法の提案
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020 2020(Dec.)
Presenter:大池勇太郎, 小形真平, 青木善貴, 中川博之, 小林一樹, 岡野浩三


Random Forest によるユーザの操作慣れ判定手法の提案
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020 2020(Dec.)
Presenter:齋藤侑, 小形真平, 岡野浩三


可読性の高いクラス図レイアウトを作成するための美的基準の調査
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第 27 回ワークショップ FOSE2020 2020(Dec.)
Presenter:大宮拓馬, 小形真平, 岡野浩三


Improving Accuracy of Automatic Deriva- tion of State Variables and Transitions from a Japanese Requirements Specification
Proceedings of the 13th International Joint Conference on Knowledge-Based Software En- gineering 2020(Sep.)
Presenter:Hiroya Ii, Kozo Okano, and Shinpei Ogata


Java model check- ing: improvement of the understanding of counterexample,
Proceedings of International Workshop on Informatics 2020 2020(Sep.)
Presenter:Marwan Bernard Hassan Chellet, Shinpei Ogata, and Kozo Okano


Deriving of Time Constants in Timed Automata for Hazard Transition Sequences for STAMP/STPA
Proceedings of the 23rd International Conference on Knowledge-Based and Intelligent Information & Engineering Systems, 2020(Sep.)
Presenter:Kozo Okano, Pan Yang, Shinpei Ogata, Keishi Okamoto


安全性解析支援のための状態遷移系に基づくハザード近接状態分析手法の提案
電子情報通信学会技術研究報告, KBSE2019 2020(Mar.)
Presenter:鈴木悠介, 小形真平, 大池勇太郎, 青木善貴, 中川博之, 小林一樹, 岡野浩三


Eclipse CheとDockerを用いたクラウドIDEによるプログラミング演習環境の構築
電子情報通信学会技術研究報告, KBSE2019 2020(Mar.)
Presenter:杉野雄大, 新村正明, 岡野浩三, 小形真平


STAMP/STPAとモデル検査の連携によるハザード遷移系列の導出手法
電子情報通信学会技術研究報告, SS2019 2020(Mar.)
Presenter:楊 盼, 岡野浩三, 小形真平, 岡本圭史


Edutainmentを指向したソフトウェア教育用フレームワークの提案
日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会 第26回ワークショップ FOSE 2019, レクチャーノート・ソフトウェア学 45 ソフトウェア工学の基礎XXVI 2019(Dec.)
Presenter:杉野雄大, 小形真平, 新村正明, 岡野浩三


word2vecとゴールモデルの階層性を利用した類似ゴール検出方法の提案
電子情報通信学会技術研究報告, KBSE2019-30 2019(Nov.)
Presenter:石川公一, 小形真平,中川博之, 岡野浩三


不具合原因分析支援のためのNuSMV反例解析手法の試案
電子情報通信学会技術研究報告, KBSE2019-30 2019(Nov.)
Presenter:大池勇太郎, 小形真平, 青木善貴, 中川博之, 小林一樹, 岡野浩三


ある組込みシステムの開発と検証のケーススタディ
電子情報通信学会技術研究報告, KBSE2019-30 2019(Nov.)
Presenter:岡野浩三, 小形真平, 夏目実希


Proposal and evaluation for property verification for Java functions with recursive data structures by SAW
Proceedings of International Workshop on Informatics 2019 2019(Sep.)
Presenter:Rin Karashima, Satoshi Harauchi, Shinpei Ogata, and Kozo Okano


A Review Assistance System for Class Diagram with Voice Assistance based on NLP
Proceedings of International Workshop on Informatics 2019 2019(Sep.)
Presenter:Masashi Nakamura, Shinpei Ogata, Kozo Okano, Toshifusa Sekizawa


Automated inspection method for a STAMP/STPA – Fallen Barrier Trap at Railroad Crossing –,
Proceedings of the 23rd International Conference on Knowledge-Based and Intelligent Information & Engineering Systems 2019(Sep.)
Presenter:Yang Pan, Kozo Okano, and Shinpei Ogata


Approach to Testing Many State Machine Models in Education
Proceedings of the 11th International Conference on Computer Supported Education (CSEDU 2019) 2019(May)
Presenter:Shinpei Ogata, Mizue Kayama, Kozo Okano:


学習済みWebサイトの操作ログに基づく有効性・効率性評価の実践
電子情報通信学会技術研究報告, KBSE2018-64 2019(Mar.)
Presenter:青木亮太, 小形真平, 岡野浩三


再帰的な構造体を用いたプログラムに対するSAWを用いた振る舞い等価性検証手法の考案と評価
第15回ソフトウェア工学の基礎ワークショップ FOSE 2018 2018(Dec.)
Presenter:辛島 凛, 原内 聡, 小形真平, 岡野浩三


ネットワーク図のモデル化とエディタの試作 ~ より円滑なネットワークインフラの運用に向けて ~
電子情報通信学会技術研究報告IN pp.117-122 2018(Nov.)
Presenter:中島徳雅, 鈴木彦文, 小形真平, 岡野浩三


Applying SAW to regression verification for C functions with recursive data structure
Proceedings of IWIN2018 2018(Sep.)
Presenter:Kozo Okano, Satoshi Harauchi


Tool to Automatically Generate a Screen Transition Model Based on a Conceptual Model
Proceedings of the 12th Joint Conference on Knowlage-Based Software Engineering 2018(Aug.)
Presenter:Yukiya Yazawa, Shinpei Ogata, Kozo Okano, Haruhiko Kaiya, and Hironori Washizaki


Towards Verification of Robot Design for Self-localization
Proceedings of 13th Haifa Verification Conference 2017(Nov.)
Presenter:Ryo Watanabe, Kozo Okano, and Toshifusa Sekizawa


Derivation of a map of variables in a loop structure
Proceedings of International Workshop on Informatics 2017 2017(Sep.)
Presenter:Kozo Okano, Shinji Kusumoto, and Yukihiro Sasaki


A method for verifying equivalence of functions in C language,
Proceedings of International Workshop on Informatics 2017 2017(Sep.)
Presenter:Satoshi Harauchi, Kozo Okano, and Shinpei Ogata


A rule-based method of stepwise evaluating class diagrams
Proceedings of IWIN2017 2017(Sep.)
Presenter:Shinpei Ogata, Kazune Miyajima, Mizue Kayama, and Kozo Okano


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)
Presenter:Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, Shin Nakajima


A New Proposal of Generating Counter-example in Model Checking Using Test Automaton
2016 pp.243-248 2016(Sep. 01)
Presenter:Chikyu Yanagisawa, Shinpei Ogata, Kozo Okano


A Method for Removing Ambiguity in Designing Sequence Diagrams for Developing Communication Programs
Proceedings of International Workshop on Informatics 2016 2016(Sep. 01)
Presenter: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)
Presenter:Shinpei Ogata, Yugo Goto, Kozo Okano


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


Safety Verification of Multiple Autonomous Systems by Formal Approach
LNCS 8696 11-18 2014(Sep.)
Presenter: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
Presenter: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 2011
Presenter: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 2008
Presenter:Kozo Okano, Shinji Kusumoto, and Yasunobu Kajita


An Evaluation Mechanism for QoS Management in Wireless Systems
Proceedings of ICPADS 2005 2005
Presenter:Behzad Bordbar, Rachid Anane, and Kozo Okano


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


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


MISC
STAMP/STPA とモデル検査の併用による単線鉄道踏切例題の 解析の効果について
日本信頼性学会誌「信頼性」,41(2):pp.89-96 2019(Mar.)
Author:岡野浩三, 岡本圭史, 小形真平


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

共同研究等希望テーマ
ソフトウェア工学一般
システム安全性検証
研究費
共同研究
2020 - 2021 , ソフトウェア・モデル検査における説明可能な反例生成に関わる基礎研究 , 国内共同研究
2018 - 2019 , IoTソフトウェアに対する反例解析を活用した自動検証技術 , 国内共同研究
2016 - 2017 , 特定機能に着目した組込みシステムソフトウェアの安全性検証技術 , 国内共同研究

受託研究
2021 - 2022 , ソフトウェア設計に関する共同研究 三菱電機(株)
2020 - 2021 , ソフトウェア設計に関する共同研究 三菱電機(株)
2020 - 2020 , プログラミング学習支援とデータ活用
2019 - 2020 , ソフトウェア設計に関する共同研究 三菱電機(株)
2019 - 2019 , プログラミング学習支援とデータ活用
2018 - 2019 , ソフトウェア設計に関する共同研究 三菱電機(株)
2018 - 2018 , ソフトウェア設計に関する共同研究 三菱電機(株)
2017 - 2017 , ソフトウェア設計に関する共同研究 三菱電機(株)
2016 - 2016 , ソフトウェア設計に関する共同研究 三菱電機(株)
2015 - 2015 , ソフトウェア設計に関する共同研究 三菱電機(株)

科学研究費補助金(研究代表者)
2021 - 2024 , 自然語解析と反例解析を活用したソフトウェア開発
2016 - 2018 , モデルと制約に基づくソフトウェア開発に関する研究
2009 - 2013 , モデル検査技術を活用したソフトウェア設計方法に関する研究
2006 - 2006 , 状態爆発するWEBアプリケーションに対するソフトウェアモデル検査
2005 - 2006 , 契約に基づいた関数型プログラム設計に対する正当性保証に関する研究

科学研究費補助金(研究分担者)
2017 - 2019 , 組み合わせテストを応用した組込みシステムの検証項目生成の研究
2014 - 2016 , 動的システムに対する組込み制御プログラムの信頼性検証に関する研究
2013 - 2017 , 多様なソフトウェア資産の収集・分析・評価と効果的な利活用の研究
研究諸活動
在外研究員等
2002-2003 , 文部科学省在外研究 , 英国Kent大学、英国 Birmingham大学

その他研究活動
2020-2022 , 電子情報通信学会ソフトウェアサイエンス研究会専門副委員長
2016-2016 , 国際会議International Workshop on Informatics IWIN General Co-Chair
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 , 電子情報通信学会ソフトウェアサイエンス研究会専門委員

管理運営実績

管理運営実績
学内兼務職
2022 - 2023 , 学科長
2021 - , 学務委員
2021 - , 副学科長
2020 - , 広報委員
2019 - , 広報委員