緒方 和博 (Kazuhiro Ogata)教授
情報科学系,知能ロボティクス領域
◆学位
慶應義塾大学工学士 (1990),慶應義塾大学工学修士 (1992),慶應義塾大学博士(工学) (1995)
◆専門分野
計算機科学、ソフトウェア工学,形式手法
◆研究キーワード
モデル検査, 書き換え, 仕様記述, 定理証明, 検証
◆研究課題
OTS/CafeOBJ法による形式検証
OTS/CafeOBJ法は,システムのモデル化,仕様記述および検証のための方法である.観測遷移機械としてシステムの数学モデルを作成する.観測遷移機械は,代数仕様言語CafeOBJで記述される.観測遷移機械が所望の性質を満足することを示す証明(証明譜と呼ぶ)をCafeOBJで記述し,証明の正しさをCafeOBJを用いて確認する.

○大規模な仕様への対応:大規模な仕様を効果的に扱えなければ、実用に耐え得る代数仕様言語を得ることはできない。大規模の仕様は,通常,多くのモジュールから構成される。このため,抽象機械でモジュールシステムを効果的に扱える必要がある。

○高速な書換え:効果的に仕様を検証したり,プログラムとして実行 (シミュレーション) するには,高速に書換えを行える必要がある。このため,抽象機械は,関数言語と同程度の処理速度を有する項書換え系の処理系を作成できる,高速な書換え機構を有する必要がある。

■研究業績

◆発表論文
Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol
Dang Duy Bui, Kazuhiro Ogata
25th International DMS Conference on Visualization and Visual Languages, -, 2019
Specification-based Testing with Simulation Relations
Canh Do Minh, Kazuhiro Ogata
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), -, 2019
Formal Specification and Model Checking of the Lim-Jeong-Park-Lee Autonomous Vehicle Intersection Control Protocol
Moe Nandi Aung, Yati Phyo, Kazuhiro Ogata
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), -, 2019
Formal Specification and Model Checking of A* Algorithm
Kazuhiro Ogata
31st International Conference on Software Engineering and Knowledge Engineering (31st SEKE), -, 2019
Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Mobile Ad Hoc Mobile Networks
Yati Phyo and Kazuhiro Ogata
25th Asia-Pacific Software Engineering Conference, -, 2018
◆書籍
Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016
Kazuhiro Ogata, Mark Lawford, Shaoying Liu, 編者, Springer, 2016
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi
Shusaku Iida, Jos?Meseguer, Kazuhiro Ogata (Eds.), 編者, Lecture Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5, 2014
◆講演・口頭発表
An attempt toward conjecturing lemmas with graphical animations of state machines
Kazuhiro Ogata
The Second International Lecture Series of School of Software and Microelectornics (SSM), Northwestern Polytechnic University , Xi'an, China, 2017/09/19
A Case Study on Extracting the Characteristics of the Reachable States of a State Machine formalizing a Communication Protocol with Inductive Logic Programing
Dung Tuan Ho, Min Zhang, Kazuhiro Ogata
25th International Conference on Inductive Logic Programming, 京都, 2015/08/20
不変性モデル検査器としてのCafeOBJ
緒方和博
2012年電子情報通信学会ソサイエティ大会, 富山市, 2012/09/11
有界モデル検査と帰納法の組合せによる NSPK 認証プロトコルの合意性
緒方和博
ソフトウェア・シンポジウム 2012 , 福井市, 2012/06/12
CafeOBJによるシステム検証
緒方和博
情報処理学会ソフトウェア工学研究会第165回研究会, JAIST, 2009/07/02

■担当講義

関数プログラミング, ソフトウェア設計論(E), 代数フォーマルメソッド(E)

■学外活動

◆学術貢献活動
Fifith IEEE International Conference on Dependable Systems and Their Applications , PC cp-chair , 2018/09/22 - 2018/09/23 , Dalian, China
18th International Conference on Formal Engineering Methods , General Chair:Shaoying Liu, Hosei University, JapanProgram Chairs:Kazuhiro Ogata, JAIST, JapanMark Lawford, McMaster University, Canada , 2016/11/14 - 2016/11/18 , TKP Conference Centre, Tokyo, Japan
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi , Jose Meseguer (UIUC)Shusaku Iida (Senshu Univ)Kazuhiro Ogata (JAIST) , 2014/04/14 - 2014/04/16 , Kanazawa

■賞等

・ BEST PAPER AWARD , The Second IEEE International Symposium on Dependable Computing and Internet of Things (DICT 2015) , 2015/11/16