![北陸先端科学技術大学院大学 [JAIST] - 研究者総覧](images/info_01.gif)
| 研究室 |
| TEL：0761-51-1239 |
研究室ホームページ |
| Japanese | English |
| リポジトリ公開資料 |
| 共同研究等のお問い合わせは， 産学官連携総合推進センター |
青木 利晃 （アオキ トシアキ） 准教授
情報科学研究科（情報科学専攻・ソフトウェア科学領域）
■学位
東京理科大学理学士（1994），北陸先端科学技術大学院大学修士(情報科学)（1996），北陸先端科学技術大学院大学博士(情報科学)（1999）
■専門分野
ソフトウェア工学, ソフトウェア科学, 形式手法, 形式検証
■研究課題
ソフトウェアの原理
プログラム意味論やプロセス代数といったソフトウェアに関連する基礎理論が古くから研究され続けており，成熟しつつある．このような基礎理論を用いて，現在のソフトウェアの原理を明らかにすることは，今後のソフトウェアの健全な発展のために重要である．そこで，現在，なんとなくソフトウェア開発で用いている記法や概念を，プログラム意味論などの枠組を用いて形式化して，その原理を明らかする研究を行っている．
形式手法/形式検証
形式手法では，数学を基礎とした言語やルールを用いて，対象となるソフトウェアを記述し検証する．これにより，なんとなくソフトウェアを開発するのではなく，数学にも基づいた解析や正しさの保証を行うことができる．また，ソフトウェアの正しさを保証する１つの手法として，厳密に記述して正しいことを証明する方法が考えられる．この方法のことは形式検証(Formal Verification)と呼ばれている．そこで，このような形式手法／検証手法を用いて正しいソフトウェアを効率的に開発する手法について研究を行っている．また，その適用対象として，主に，オブジェクト指向分析・設計法，組み込みソフトウェア開発に焦点を当てている．
■研究業績
◇著書
- 青木利晃, 9章 組込みソフトウェアの静的検証技術(pp.271-307)，沢田 篤史，et al.，組込みソフトウェア開発技術, CQ出版, ISBN 978-4-7898-4548-9
- 知識ベース, 7群1編2章5節 UML/ステートチャート，青木利晃，電子情報通信学会，pp.35-44
- SPINによる設計モデル検証，吉岡信和，青木利晃，田原康之，近代科学社，2008
◇発表論文
- Model Checking of OSEK/VDX OS Design Models based on Environment Modeling，Kenro Yatake, Toshiaki Aoki，ICTAC，Sep 25, 2012
- SMT-based enumeration of Object Graphs from UML Class Diagrams，Kenro Yatake, Toshiaki Aoki，UML&FM，August 27, 2012
- UMLに基づくリアルタイムOS検証のための環境自動生成法，矢竹健朗，青木利晃，コンピュータソフトウェア，29，3，121-142，8/20, 2012
◇講演発表
- モデル検査器により出力された反例に基づく誤り特定に関する研究，陳適, 青木利晃，情報処理学会 第177回ソフトウェア工学研究会
- 形式手法の研究と実践からざっくばらんに…-産業界での可能性や今後の展望-，青木利晃，フォーマルメソッド普及促進セミナー2011 in 札幌，2011/7/22．
- モデル検査手法の普及活動とその応用，青木利晃，SPI 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
- 情報処理学会 組込みシステムシンポジウム，プログラム委員長，2006/10/19-21
◇その他の国際・国内貢献等
- 電子情報通信学会，ソフトウェアサイエンス研究会 専門委員，2008/04/01 - 2010/03/31
- 日本ソフトウェア科学会，コンピュータソフトウェア 編集委員，2007/04/01 -
- 情報処理学会，組込みシステム研究会 運営委員，2007/04/01 - 2010/03/31
■賞等
- 山下記念研究賞受，情報処理学会，2006
- 組込みソフトウェアシンポジウム優秀論文賞，情報処理学会 ソフトウェア工学研究会，2005
■共同研究等希望テーマ
- 形式手法，形式検証
- オブジェクト指向開発
- 組み込みシステム開発