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

■研究業績

◆発表論文
Frequency probabilistic risk assessment using coloured petri nets for telemedicine
K. Fujita, K. Hiraishi, T. Aoki
IEEE International Conference on Industrial Engineering and Engineering Management, 2020-December, 1098-1102, 2020
Comprehensive Robustness Evaluation of File Systems with Model Checking
Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo
Proceedings - 2020 IEEE 20th International Conference on Software Quality, Reliability, and Security, QRS 2020, 99-110, 2020
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
Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems.
Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita
100-109, 2020
Multiple conformance to hybrid-automata-modelled requirements for detecting indoor temperature anomalies
Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
Indoor and Built Environment, -, 2020
◆Misc
自動運転システムにおける画像を対象とした形式仕様記述言語BBSLの提案
田中健人, 青木利晃, 川上大介, 千田伸男, 河井達治, 冨田尭
情報処理学会研究報告(Web), 2020, SE-205, -, 2020
Event-Bに基づいた鉄道システムの実践的な形式化と検証
太田十字光, 青木利晃
情報処理学会研究報告(Web), 2019, SE-203, -, 2019
区間解析法とモンテカルロ法の連携によるSimulinkテストケースの自動生成
石井 大輔, 野村 亮太, 八田 竜起, 冨田 尭, 青木 利晃
日本ソフトウェア科学会第35回大会, -, 2018
「IoT,AI,ビッグデータと安全工学」形式手法と安全性
青木利晃
安全工学研究発表会講演予稿集, 51st, -, 2018
複合的因果関係分析手法を用いた遠隔診療の定量的安全性評価 (システム数理と応用)
藤田 健治, 青木 利晃, 平石 邦彦
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 117, 301, 89-94, 2017
◆講演・口頭発表
車載システム開発における形式手法実践の現状と課題
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