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

■研究業績

◆発表論文
A framework for assume-guarantee regression verification of evolving software
Hoang Viet Tran, Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki
Science of Computer Programming, 193, -, 2020
Multiple conformance to hybrid-automata-modelled requirements for detecting indoor temperature anomalies
Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
Indoor and Built Environment, -, 2020
Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models.
Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
IEICE Transactions, 103-A, 2, 451-461, 2020
Model checking of in-vehicle networking systems with CAN and FlexRay.
Xiaoyun Guo, Toshiaki Aoki, Hsin-Hung Lin
Journal of Systems and Software, 161, -, 2020
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
◆Misc
区間解析法とモンテカルロ法の連携によるSimulinkテストケースの自動生成
石井 大輔, 野村 亮太, 八田 竜起, 冨田 尭, 青木 利晃
日本ソフトウェア科学会第35回大会, -, 2018
複合的因果関係分析手法を用いた遠隔診療の定量的安全性評価 (システム数理と応用)
藤田 健治, 青木 利晃, 平石 邦彦
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 117, 301, 89-94, 2017
Simulinkモデルに対するテストスイート自動生成
冨田 尭, 石井 大輔, 青木 利晃
第14回ディペンダブルシステムワークショップ (DSW’16), -, 2016
Java Pathfinderにおける弱公平性条件の実装
太田 十字光, 田辺 良則, 青木 利晃
日本ソフトウェア科学会大会論文集, 33, 461-469, 2016
再利用のためのRTLからの関数コード生成手法 (VLSI設計技術)
立岡 真人, 青木 利晃, 金子 峰雄
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 113, 454, 171-176, 2014
◆講演・口頭発表
車載システム開発における形式手法実践の現状と課題
2018
「IoT,AI,ビッグデータと安全工学」形式手法と安全性
安全工学研究発表会講演予稿集, 2018
Java Pathfinderにおける弱公平性条件の実装
日本ソフトウェア科学会大会講演論文集(CD-ROM), 2016

■担当講義

Software Process Design for Highly Dependable Embedded Systems, Software Design Methodology, Transdisciplinary Session I, 高信頼組込みシステム開発プロセス設計, ソフトウェア設計論, 異分野「超」体験セッションⅠ, ソフトウェア検証論

■学外活動

◆所属学会
情報処理学会, 電子情報通信学会, 日本ソフトウェア科学会
◆学術貢献活動
International Workshop on Software Technologies for Future Dependable Distributed Systems , Workshop Co-Chair , 2009 , Waseda University
SPLC 2007 Doctoral Symposium , Symposium co-chair , 2007
情報処理学会 組込みシステムシンポジウム , プログラム委員長 , 2006 - 2006
◆社会貢献活動
・ 14th International Symposium on Theoretical Aspects of Software Engineering , PC chair 2020
・ 14th International Conference on Formal Engineering Methods , Program Co-Chair 2012 - 2012

■賞等

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