北陸先端科学技術大学院大学 [JAIST] - 研究者総覧
現在ページ トップページ 検索結果> 研究者紹介

研究者紹介

研究室
 
TEL:0761-51-1239
研究室ホームページ
領域ホームページ
 

Japanese

リポジトリ公開資料

共同研究等のお問い合わせは, 産学官連携総合推進センター

 

 

青木 利晃 (アオキ トシアキ) 教授
情報科学系、セキュリティ・ネットワーク領域

■学位

東京理科大学理学士(1994),北陸先端科学技術大学院大学修士(情報科学)(1996),北陸先端科学技術大学院大学博士(情報科学)(1999)

■専門分野

ソフトウェア工学, ソフトウェア科学, 形式手法, 形式検証

■研究課題

ソフトウェアの原理
プログラム意味論やプロセス代数といったソフトウェアに関連する基礎理論が古くから研究され続けており,成熟しつつある.このような基礎理論を用いて,現在のソフトウェアの原理を明らかにすることは,今後のソフトウェアの健全な発展のために重要である.そこで,現在,なんとなくソフトウェア開発で用いている記法や概念を,プログラム意味論などの枠組を用いて形式化して,その原理を明らかする研究を行っている.
形式手法/形式検証
形式手法では,数学を基礎とした言語やルールを用いて,対象となるソフトウェアを記述し検証する.これにより,なんとなくソフトウェアを開発するのではなく,数学にも基づいた解析や正しさの保証を行うことができる.また,ソフトウェアの正しさを保証する1つの手法として,厳密に記述して正しいことを証明する方法が考えられる.この方法のことは形式検証(Formal Verification)と呼ばれている.そこで,このような形式手法/検証手法を用いて正しいソフトウェアを効率的に開発する手法について研究を行っている.また,その適用対象として,主に,オブジェクト指向分析・設計法,組み込みソフトウェア開発に焦点を当てている.

■研究業績

◇著書

  • Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods,Toshiaki Aoki, Kenji Taguchi (Eds.),Lecture Notes in Computer Science 7635, Springer,2012
  • 青木利晃, 9章 組込みソフトウェアの静的検証技術(pp.271-307),沢田 篤史,et al.,組込みソフトウェア開発技術, CQ出版, ISBN 978-4-7898-4548-9
  • 知識ベース, 7群1編2章5節 UML/ステートチャート,青木利晃,電子情報通信学会,pp.35-44

全件表示

◇発表論文

  • SMT-based enumeration of Object Graphs from UML Class Diagrams,Kenro Yatake, Toshiaki Aoki,UML&FM,August 27, 2012
  • Model Checking of OSEK/VDX OS Design Models based on Environment Modeling,Kenro Yatake, Toshiaki Aoki,ICTAC,Sep 25, 2012
  • UMLに基づくリアルタイムOS検証のための環境自動生成法,矢竹健朗,青木利晃,コンピュータソフトウェア,29,3,121-142,8/20, 2012

全件表示

◇講演発表

  • 形式手法を産業界で実践するためのアプローチ,青木利晃,組込み総合技術展専門セミナー
  • 聴覚特性を利用した音響電子透かし「大事なデータを音に紛れ込ませることはできるか?」,鵜木祐史,電気関係学会北陸支部連合大会,金沢工業大学,2015/09/12
  • 開発現場における形式手法の実践-商用車載オペレーティングシステムへの適用-,青木利晃,第17回組込みシステム開発技術展

全件表示

■担当講義

高信頼ソフトウェア開発プロセス設計,ソフトウェア設計論,ソフトウェア検証論

■学外活動

◇国際会議主催状況

  • 14th International Conference on Formal Engineering Methods,Program Co-Chair,November 12-16, 2012,Kyote, JAPAN
  • International Workshop on Software Technologies for Future Dependable Distributed Systems,Workshop Co-Chair,2009/03/17,Waseda University
  • SPLC 2007 Doctoral Symposium,Symposium co-chair,Sep. 10, 2007

全件表示

◇審議会等への参画状況

  • 情報処理推進機構,ソフトウェア高信頼化センター ソフトウェア高信頼化推進委員会委員,2015-2016年度

◇その他の国際・国内貢献等

  • 日本ソフトウェア科学会 ソフトウェア工学の基礎ワークショップ(FOSE2015),プログラム委員長
  • 電子情報通信学会,ソフトウェアサイエンス研究会 専門委員,2008/04/01 - 2010/03/31
  • 情報処理学会 組込みシステムシンポジウム,プログラム委員,2007/04/01 -

全件表示

■賞等

  • 山下記念研究賞受,情報処理学会,2006
  • 組込みソフトウェアシンポジウム優秀論文賞,情報処理学会 ソフトウェア工学研究会,2005

■共同研究等希望テーマ

  • 形式手法,形式検証
  • オブジェクト指向開発
  • 組み込みシステム開発