青木 利晃 (AOKI, Toshiaki)教授
融合科学系, 情報科学系,セキュリティ・ネットワーク領域
◆学位
東京理科大学理学士(1994),北陸先端科学技術大学院大学修士(情報科学)(1996),北陸先端科学技術大学院大学博士(情報科学)(1999)
◆職歴
2016/10 - : 北陸先端科学技術大学院大学 , 先端科学技術研究科 , 教授
2009/03 - 2016/09 : 北陸先端科学技術大学院大学 , 情報科学研究科 , 助教授
2006/03 - 2009/02 : 北陸先端科学技術大学院大学 , 安心電子社会研究センター , 特任助教授
2001/12 - 2005/03 : 科学技術振興事業団 , さきがけ研究21「機能と構成」領域 , 研究員
1999/04 - 2006/02 : 北陸先端科学技術大学院大学 , 情報科学研究科 , 助手
◆専門分野
ソフトウェア工学, ソフトウェア科学, 形式手法, 形式検証
◆研究キーワード
形式仕様, 定理証明, モデル検査, ソフトウェア工学, ソフトウェアテスト, 車載システム, 形式検証, 形式手法
◆研究課題
ソフトウェアの原理
プログラム意味論やプロセス代数といったソフトウェアに関連する基礎理論が古く から研究され続けており,成熟しつつある.このような基礎理論を用いて,現在の ソフトウェアの原理を明らかにすることは,今後のソフトウェアの健全な発展のた めに重要である.そこで,現在,なんとなくソフトウェア開発で用いている記法や 概念を,プログラム意味論などの枠組を用いて形式化して,その原理を明らかする 研究を行っている.
形式手法/形式検証
形式手法では,数学を基礎とした言語やルールを用いて,対象となるソフトウェア を記述し検証する.これにより,なんとなくソフトウェアを開発するのではなく, 数学にも基づいた解析や正しさの保証を行うことができる.また,ソフトウェアの 正しさを保証する1つの手法として,厳密に記述して正しいことを証明する方法が 考えられる.この方法のことは形式検証(Formal Verification)と呼ばれている. そこで,このような形式手法/検証手法を用いて正しいソフトウェアを効率的に開 発する手法について研究を行っている.また,その適用対象として,主に,オブジェ クト指向分析・設計法,組み込みソフトウェア開発に焦点を当てている.

■研究業績

◆発表論文
Reducing false positives of static analysis for SEI CERT C coding standard.
Thu Trang Nguyen,Pattaravut Maleehuan,Toshiaki Aoki,Takashi Tomita,Iori Yamada
Proceedings of the Joint 7th International Workshop on Conducting Empirical Studies in Industry and 6th International Workshop on Software Engineering Research and Industrial Practice, CESSER-IP@ICSE 2019, Montreal, QC, Canada, May 27, 2019, 41-48, 2019
Conformance Testing of Schedulers for DSL-based Model Checking.
Nhat-Hoa Tran,Toshiaki Aoki
Model Checking Software - 26th International Symposium, SPIN 2019, Beijing, China, July 15-16, 2019, Proceedings, 208-225, 2019
Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies.
Nhat-Hoa Tran,Yuki Chiba,Toshiaki Aoki
IEICE Transactions, 102-D, 7, 1280-1295, 2019
A scalable Monte-Carlo test-case generation tool for large and complex simulink models.
Takashi Tomita,Daisuke Ishii,Toru Murakami,Shigeki Takeuchi,Toshiaki Aoki
Proceedings of the 11th International Workshop on Modelling in Software Engineerings, MiSE@ICSE 2019, Montreal, QC, Canada, May 26-27, 2019, 39-46, 2019
車載システム開発における形式手法実践の現状と課題
青木利晃
システム/制御/情報, 62, 4, 134‐140-140, 2018/04
◆Misc
ウインターワークショップ2008・イン・道後開催報告
阿萬裕久, 青木利晃, 沢田篤史, 山本晋一郎, 渥美紀寿, 白銀純子, 浦本直彦, 松塚貴英, 羽生田栄一, 鷲崎弘宜, 野中誠, 吉岡信和, 田原康之
情報処理学会研究報告, 2008, 55(SE-160 EMB-9), 65-72, 2008/06/12
組込みシステムシンポジウム2006実施報告
沢田篤史, 青木利晃, 冨山宏之, 久保秋真
情報処理学会研究報告, 2007, 52(SE-156 EMB-5), 27-32, 2007/05/28
「ウィンターワークショップ2007・イン・那覇」開催報告
松塚貴英, 沢田篤史, 青木利晃, 福安直樹, 妻木俊彦, 中村友昭, 浦本直彦, 羽生田栄一, 鷲崎弘宜
情報処理学会研究報告, 2007, 52(SE-156 EMB-5), 19-25, 2007/05/28
形式的手法最前線―拠点の活動とねらい
青木利晃, 荒木啓二郎, 片山卓也, 木下佳樹, 中島震
情報処理学会シンポジウム論文集, 2006, 9, 158-159, 2006/10/19
組み込みシステム開発への形式的手法の適用
青木利晃
情報処理学会シンポジウム論文集, 2003, 13, 126-127, 2003/10/16
◆講演・口頭発表
車載システム開発における形式手法実践の現状と課題
青木利晃
2018/12/13
「IoT,AI,ビッグデータと安全工学」形式手法と安全性
青木利晃
安全工学研究発表会講演予稿集, 2018/11/27
複合的因果関係分析手法を用いた遠隔診療の定量的安全性評価
藤田健治, 青木利晃, 平石邦彦
電子情報通信学会技術研究報告, 2017/11/09
Java Pathfinderにおける弱公平性条件の実装
太田十字光, 田辺良則, 田辺良則, 青木利晃
日本ソフトウェア科学会大会講演論文集(CD-ROM), 2016
遠隔診療におけるリスクアセスメント手法の提案
藤田健治, 青木利晃
情報処理学会研究報告(Web), 2015/08/21

■担当講義

ソフトウェア検証論, 異分野「超」体験セッションⅠ, ソフトウェア設計論, 高信頼組込みシステム開発プロセス設計

■学外活動

◆所属学会
日本ソフトウェア科学会, 電子情報通信学会, 情報処理学会
◆学術貢献活動
14th International Conference on Formal Engineering Methods , Program Co-Chair , 2012/11/12 - 2012/11/16 , Kyote, JAPAN
SPLC 2007 Doctoral Symposium , Symposium co-chair , 2007/09/10
International Workshop on Software Technologies for Future Dependable Distributed Systems , Workshop Co-Chair , 2009/03/17 , Waseda University

■賞等

・ 第十二回善吾賞 , 青木利晃,川上大介,千田伸男,冨田尭 , ソフトウェアテスト技術振興協会 , 2019/03
・ Best Paper Award , Nhat-Hoa Tran, Yuki Chiba and Toshiaki Aoki , 24th Asia-Pacific Software Engineering Conference , 2017/12
・ 山下記念研究賞受賞 , 青木利晃 , 情報処理学会 , 2006/03