AOKI, Toshiaki Professor
Division of Transdisciplinary Sciences, School of Information Science, Security and Networks Area
◆Degrees
B.S. from Science University of Tokyo(1994), M.S. and Ph.D. from Japan Advanced Institute of Science and Technology(1996, 1999)
◆Professional Experience
2016 - : Japan Advanced Institute of Science and Technology , Graduate School of Advanced Science and Technology , Professor
2009 - 2016 : Japan Advanced Institute of Science and Technology , School of Information Science , Associate Professor
2006 - 2009 : Japan Advanced Institute of Science and Technology , Research Center on Trustworthy e-Society , Research Associate Professor
2001 - 2005 : 科学技術振興事業団 , さきがけ研究21「機能と構成」領域 , 研究員
1999 - 2006 : Japan Advanced Institute of Science and Technology , School of Information Science , Associate
◆Specialties
Software
◆Research Keywords
Formal Method, Formal Verification, Automotive System, Software Testing, Software Engineering, Model Checking, Theorem Proving, Formal Specification
◆Research Interests
Principle of Software
Fundamental theories for software are studying for a long time. Some of them are getting matured such as program semantics and process algebra. To promise bright future of software, it is important to find the principles of software based on those theories. Unfortunately, today’s software is developed without such principles. We should change this style of software developments into more scientific ones which are integrated on the mathematics. Thus, we are challenging to establish such fundamental principles of software.
Formal Method/Formal Verification
Formal methods represent a development style of software based on mathematics. We describe its specification and design in not natural language but languages based on mathematical theories such as sets and functions. That not only makes the specification and design rigorous but also allows us to precisely analyze them, prove their correctness and automatically generate source codes. One way to provide correctness with software is that we describe it rigorously, then we prove its correctness. That is called 'formal verification' of software. We are researching how we can develop correct software effectively using the formal methods and formal verification. Especially, we focus on embedded systems and object-oriented design for their application targets.

■Publications

◆Published Papers
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
Practical formalization and verification of railway system based on Event-B
太田十字光, 青木利晃
情報処理学会研究報告(Web), 2019, SE-203, -, 2019
区間解析法とモンテカルロ法の連携によるSimulinkテストケースの自動生成
石井 大輔, 野村 亮太, 八田 竜起, 冨田 尭, 青木 利晃
日本ソフトウェア科学会第35回大会, -, 2018
「IoT,AI,ビッグデータと安全工学」形式手法と安全性
青木利晃
安全工学研究発表会講演予稿集, 51st, -, 2018
Quantitative safety assessment of telemedicine using the MCCA
藤田 健治, 青木 利晃, 平石 邦彦
電子情報通信学会技術研究報告 = IEICE technical report : 信学技報, 117, 301, 89-94, 2017
◆Conference Activities & Talks
車載システム開発における形式手法実践の現状と課題
2018
「IoT,AI,ビッグデータと安全工学」形式手法と安全性
安全工学研究発表会講演予稿集, 2018
Quantitative safety assessment of telemedicine using the MCCA
電子情報通信学会技術研究報告, 2017
Java Pathfinderにおける弱公平性条件の実装
日本ソフトウェア科学会大会講演論文集(CD-ROM), 2016
A Risk Assessment Method for Telemedicine
情報処理学会研究報告(Web), 2015

■Teaching Experience

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

■Contributions to  Society

◆Academic Society Affiliations
Information Processing Society of Japan, The Institute of Electronics, Information and Communication Engineers, Japan Society for Software Science and Technology
◆Academic Contribution
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
◆Social Contribution
・ 14th International Symposium on Theoretical Aspects of Software Engineering , PC chair 2020
・ 14th International Conference on Formal Engineering Methods , Program Co-Chair 2012 - 2012

■Academic  Awards

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