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.
JST CREST Project: Formal Methods and Verification Tools for Next-generation Automotive System Platforms
We are looking for the members of this project. Let us know if you are interested in.
Developing Safe and Secure Systems
- Modern systems: autonomous driving, Al systems, smart city, block- chain, quantum computing, etc.
- Traditional Modern: transition to modern system development.
Development and Verification based on Computer Science
- Ensure safety and security scientifically.
- Formal methods, formal verification, and beyond.
Challenge to Industrial Application
- Software systems in industry and society.
- Automotive systems, space systems, important nfrastructures, etc.
Challenge
-
Large and Complex
We focus on real systems.
-
Undecidable
We focus on practical treatment of undecidable problems.
-
Uncertainty
We focus on uncertainty introduced by Al.
-
Quality Assurance
We focus on explanation that systems are of high quality.
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.
Examples of Research Topics
Software is becoming more and more diversified. AI is a very hot topic currently, and it is realized as software. Autonomous driving is attracting us, and software plays an important role in it. DX and digitalization are becoming a main stream of our society, and software is an important foundation for realizing them. We are working on such modern systems. We show examples of our research items as follows.
Reliability and safety verification of AI systems.
Formal specification and verification for complex data such as images and videos.
Verification of modern operating systems.
Verification for model-based development with MATLAB/Simulink.
Practical verification of automotive system programs.
Quality assurance of open sources.
Risk assessment for block-chain systems.
Model-based development for spacecraft.
Reliability and safety verification for mobile file systems.
Application of quantum computing to classical program verification.