TOP Page >  Profile

Lab
 
To Lab's Site
 
 

English

Full text / JAIST Repository

 

 

Kazuhiro Ogata Associate Professor
School of Information Science(Department of Information Science・Theoretical Information Science)

■Degrees

Ph.D.form Keio University (1995)

■Specialties

Software engineering, Formal methods, Verification

■Research Keywords

モデル検査,書き換え,仕様記述,定理証明,検証

■Research Interests

Formal verification with the OTS/CafeOBJ method
The OTS/CafeOBJ method is a modeling, specification and verification method for systems. Observational transition systems, or OTSs are used as mathematical models of systems. OTSs are written in CafeOBJ, an algebraic specification language/system, and it is verified that OTSs satisfy properties by writing proof plans called proof scores in CafeOBJ and checking them with CafeOBJ.

■Publications

◇Published Papers

  • Automating Invariant Verification of Behavioral Specifications,Masahiro Nakano, Kazuhiro Ogata, Masaki Nakamura, and Kokichi Futatsugi ,In Proceedings of The Sixth IEEE International Conference on Quality Software (QSIC2006),pp. 49-56,Oct. 2006
  • A complete specification transformation from OTS/CafeOBJ to OTS/Maude,Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi,信学技報 IEICE Technical Report,SS2006,13,pp. 1-6,JUNE 2006
  • Chocolat/SMV: A Translator from CafeOBJ into SMV,Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi, Proceedings of the 6th International Conference on Parallel and Distributed Computing Applications and Technologies (6th PDCAT), IEEE Computer Society Press,pp.416-420,Dec 2005

Display All

◇Lectures and Presentations

  • 代数仕様言語CafeOBJによる実時間システムの仕様記述と検証 - tmed two-process race の仕様記述と検証 -,清野貴博、緒方和博、二木厚吉,電子情報通信学会ソフトウェアサイエンス研究会(1月研究集会)
  • Specification and verification of a single-track railroad signaling in CafeOBJ,Takahiro Seino, Kazuhiro Ogata, Kokichi Futatsugi,200 International Technical Conference on Circuts/Systems, Computers and Communications (ITC-CSCC 2000)
  • The evaluation strategy for head normal form with and without on-demand flags,Masaki Nakamura, Kazuhiro Ogata,The 3rd International Workshop on Rewriting Logic and its Applications (WRLA 2000)

Display All

■Extramural Activities

◇Other Activities

  • International Conference on Formal Engineering Methods,Co-workshop Chair
  • IEICE,Editor in Chief, Special Section of Formal Approach, IEICE,2012/03/01 - 2013/02/28