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

■研究業績

◆発表論文
Specification Based Testing of Object Detection for Automated Driving Systems via BBSL.
Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida
ENASE, 250-261, 2023
Compaction of Spacecraft Operational Models with Metamodeling Domain Knowledge.
Kazunori Someya, Toshiaki Aoki, Naoki Ishihama
ENASE, 102-113, 2023
Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS), -, 2022
SMT-Based Model Checking of Industrial Simulink Models.
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
ICFEM, 156-172, 2022
Compliance SSI System Property Set to Laws, Regulations, and Technical Standards.
Charnon Pattiyanon, Toshiaki Aoki
IEEE Access, 10, 99370-99393, 2022
◆Misc
Selected papers from the 14th international symposium on Theoretical Aspects of Software Engineering.
Toshiaki Aoki, Qin Li 0002
Science of Computer Programming, 219, 102821-102821, 2022
Compositional Test Generation of Industrial Synchronous Systems.
Daisuke Ishii, Takashi Tomita, Kenji Onishi, Toshiaki Aoki
CoRR, abs/2112.05411, -, 2021
Approximate Translation from Floating-Point to Real-Interval Arithmetic.
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
CoRR, abs/2112.02804, -, 2021
自動運転システム開発におけるシミュレーション検証のためのテストケース生成手法の提案
鈴木玄貴, 冨田尭, 青木利晃, 河井達治, 川上大介, 千田伸男
情報処理学会研究報告(Web), 2021, SE-207, -, 2021
宇宙機自動ドッキングシステムを対象としたMBSE手法と物理シミュレーションとを連携させた安全性分析・評価手法の提案
染谷一徳, 染谷一徳, 和田恵一, 河津要, 青木利晃
情報処理学会全国大会講演論文集, 83rd, 1, -, 2021
◆書籍
◆講演・口頭発表
車載システム開発における形式手法実践の現状と課題
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