Realize Safety and Security by Advanced Science and Technology

AOKI Laboratory
Professor：AOKI Toshiaki

E-mail：
［Research areas］
software engineering, software science
［Keywords］
formal methods, formal verification, testing, model checking, theorem proving, automotive systems, safety critical systems

Skills and background we are looking for in prospective students

Sound logical thinking skill is necessary. A student who is good at mathematics is better. Good program skill is not mandatory but is advantageous.

What you can expect to learn in this laboratory

You can learn advanced science and technology for real software/system developments. Our laboratory focuses on practical applications of scientific techniques such as formal methods and formal verification to system/software developments. Our target is not a toy problem like calculating Fibonacci series but a real system like an automotive system. In this case, you need to identify an essential problem of a real system and solve it scientifically. This is very challenging because there are many problems in the real system and they are non-trivial, usually unknown and mysterious. I am quite sure that getting an ability to do this is useful not only for researchers but also for professional practitioners.

【Job category of graduates】 Electric company, automotive company, IT company, university, national institute

Research outline

[Realize Correct Software]

Software is used everywhere in our society today. It is used not only in personal computers but also in mobile phones, electric appliances, cars and airplanes. Software is closely related to our daily life and we cannot live without it anymore. On the other hand, the quality of software is becoming a big concern recently. The bugs of software can give serious damage to our society like causing big loss of money, confusion of daily life, loss of life, and so on. In fact, such incidents have been frequently reported these days. One may think that it is strange that buggy software is used in our society. Actually, that is unavoidable at this moment since there is no way to develop systems without any bug. Thus, it is very important to establish a method to develop correct software, that is, software with no bug, for realizing safe and secure society.

[Formal Methods/Formal Verification]

Typical and hopeful way to realize correct software is to use formal methods and formal verification. Formal methods is 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. Proving the correctness of software is called formal verification. However, there is a big gap between the formal methods/formal verification and real systems. We are working on bridging the gap between them.

[Challenge to Industrial Application]

Our research target is 'software of our society'. In order to deal with such real software, we are conducting joint-projects with industrial partners, especially, automotive companies. Cars are dangerous vehicles which are close to our daily life and many human lives are lost every year due to traffic accidents. Challenge to realize advanced safety as well as correct control using software is being made. Our laboratory is one of the best laboratories in the world which are collaborating with automotive companies and succeeded in verifying real software used in real cars. Recently, key technologies such as AI and blockchain are used for safety critical systems and our social infrastructures. DX is being accelerated. Software is becoming more and more important to realize them. We continue research to realize safe and secure society with advanced science and technology not only in automotive field but also the other ones which play important roles of our society.

Key publications

1. Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita: Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems, 25th IEEE Pacific Rim International Symposium on Dependable Computing, pp.100-109, 2020.
2. Toshiaki Aoki, Makoto Satoh, Mitsuhiro Tani, Kenro Yatake, Tomoji Kishi: Combined Model Checking and Testing Create Confidence - A Case on Commercial Automotive Operating System, Chapter 5, pp.109-132, Cyber-Physical System Design from an Architecture Analysis Viewpoint: Springer, 2017.
3. Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi and Fumio Narisawa: Modeling Safety Requirements of ISO 26262 using Goal Trees and Patterns, International Workshop on Formal Techniques for Safety-Critical Systems, Springer, pp.206-221, 2015.

Equipment

Personal computers and networks.