本文へジャンプ

Realize Safety and Security by Advanced Science and Technology

AOKI Laboratory
Professor:Toshiaki Aoki

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. 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, 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.
  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. Kenro Yatake and Toshiaki Aoki: Automatic Generation of Model Checking Scripts based on Environment Modeling, The 17th International SPIN Workshop on Model Checking of Software, pp.58-75, 2010.

Equipment

Personal computers and networks.

Teaching policy

We supervise students so that they can acquire the following skills. 1)They can understand essential points of problems existing in real systems. 2) They can solve the problems scientifically. In order to acquire them, we frequently discuss with the students based on concrete examples, hopefully, real products at early stage of research. Once the essential points are identified, the research progress is reported regular laboratory seminar. The seminar is held every week and one student is assigned to each time usually. Each student is supposed to report the progress once a month.

[Website] URL:http://www.jaist.ac.jp/is/labs/aoki-lab/

PageTop