トップページ  >  教員個別情報
緒方　和博 （OGATA, Kazuhiro）教授, 情報社会基盤研究センター長
情報科学, コンピューティング科学研究領域, 情報社会基盤研究センター
◆学位
慶應義塾大学工学士 (1990)，慶應義塾大学工学修士 (1992)，慶應義塾大学博士(工学) (1995)
◆専門分野
ソフトウェア
◆研究キーワード
検証, 定理証明, 仕様記述, 書き換え, モデル検査
◆研究課題
OTS/CafeOBJ法による形式検証
OTS/CafeOBJ法は，システムのモデル化，仕様記述および検証のための方法である．観測遷移機械としてシステムの数学モデルを作成する．観測遷移機械は，代数仕様言語CafeOBJで記述される．観測遷移機械が所望の性質を満足することを示す証明(証明譜と呼ぶ)をCafeOBJで記述し，証明の正しさをCafeOBJを用いて確認する．

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

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

■研究業績

◆発表論文
Formal analysis of RFC 8120 authentication protocol for HTTP under different assumptions
Naomi Okumura, Kazuhiro Ogata, Yoichi Shinoda
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 53, 102529-102529, 2020
A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions
Kazuhiro Ogata
FRONTIERS OF COMPUTER SCIENCE, 13, 1, 51-72, 2019
Formal analysis of a security protocol for e-passports based on rewrite theory specifications
Manjukeshwar Reddy Mandadi, Varuneshwar Reddy Mandadi, Kazuhiro Ogata
JOURNAL OF INFORMATION SECURITY AND APPLICATIONS, 42, 71-86, 2018
Prove it! Inferring Formal Proof Scripts from CafeOBJ Proof Scores
Adrian Riesco, Kazuhiro Ogata
ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 27, 2, 6-32, 2018
From hidden to visible: A unified framework for transforming behavioral theories into rewrite theories
Min Zhang, Kazuhiro Ogata
THEORETICAL COMPUTER SCIENCE, 722, 52-75, 2018
◆Misc
A divide and conquer approach to leads-to-model checking
Yati Phyo, Canh Minh Do, Ogata Kazuhiro
ITNOW, 63, 2, 66-, 2021
OTS/CafeOBJ法によるマルチタスク実時間システムの形式的検証 (システム数理と応用)
東 周輝, 中村 正樹, 榊原 一紀, 緒方 和博
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 119, 470, 25-30, 2020
OTS/CafeOBJ法によるマルチタスク実時間システムの仕様記述 (システム数理と応用)
東 周輝, 中村 正樹, 榊原 一紀, 緒方 和博
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 118, 499, 13-18, 2019
ソフトウェアサイエンス研究会（SS研）の紹介
緒方 和博
情報・システムソサイエティ誌, 21, 3, 8-9, 2016
構成子に基づく順序ソートパラメータ化仕様の十分完全性について (ソフトウェアサイエンス)
中村 正樹, ガイナ ダニエル ミルチェア, 緒方 和博, 二木 厚吉
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 114, 510, 1-6, 2015
◆書籍
Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016
編者(編著者) , 312, Springer, 2016
Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi
編者(編著者) , Lecture Notes in Computer Science 8373, Springer 2014, ISBN 978-3-642-54623-5, 2014
電子情報通信学会「知識ベース」
分担執筆, 2010
◆講演・口頭発表
An attempt toward conjecturing lemmas with graphical animations of state machines
The Second International Lecture Series of School of Software and Microelectornics (SSM), Northwestern Polytechnic University, Xi'an, China, 2017
A Case Study on Extracting the Characteristics of the Reachable States of a State Machine formalizing a Communication Protocol with Inductive Logic Programing
25th International Conference on Inductive Logic Programming, 京都, 2015
不変性モデル検査器としてのCafeOBJ
2012年電子情報通信学会ソサイエティ大会, 富山市, 2012
有界モデル検査と帰納法の組合せによる NSPK 認証プロトコルの合意性
ソフトウェア・シンポジウム 2012, 福井市, 2012
CafeOBJによるシステム検証
情報処理学会ソフトウェア工学研究会第165回研究会, JAIST, 2009

■担当講義

Information Processing Theory(E), Algebraic Formal Methods(E), Software Design Methodology(E), Functional Programming, 情報処理論(E), 代数フォーマルメソッド(E), ソフトウェア設計論(E), 関数プログラミング

■学外活動

◆学術貢献活動
Review Editor on the Editorial Board of Computer Security , Frontiers in Computer Science , 2020
PC co-chair , 32nd International Conference on Software Engineering & Knowledge Engineering , 2020 - 2020
PC co-chair , Fifith IEEE International Conference on Dependable Systems and Their Applications , 2018 - 2018 , Dalian, China
◆審議会等への参画状況
・ 石川県教育委員会 , 「いしかわ高校科学グランプリ」における運営指導委員 , 2014-

■賞等

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