Towards Realization of Highly Safe and Reliable Systems

TOMITA Laboratory
Associate Professor：TOMITA Takashi

E-mail：
［Research areas］
formal methods, computer science, software engineering, digital transformation (DX)
［Keywords］
model checking, program/specification verification, model/program/test generation

Skills and background we are looking for in prospective students

Basic mathematical knowledge, information literacy, IT skills, and logical thinking skills are necessary. Depending on your research theme, programming skills and/or basic knowledge on computation theory, mathematical logic, probability theory and/or statistics are preferred.

What you can expect to learn in this laboratory

You will learn advanced theories and techniques to analyze and develop software/systems and abstract and structural thinking skills to identify and summarize the essence of problems, and will be able to propose reasonable solutions for the problems by utilizing (or extending, if necessary) the theories and techniques.

Research outline

[Formal Methods]

Formal methods are a kind of methods for specification, development and verification of software/hardware, by using languages, techniques and tools based on mathematics.
Formal methods can strictly ensure the safety and reliability of software/hardware because they are supported by the validity of mathematics. Therefore, they are often applied to the development and verification for many safety- and reliability- critical systems, e.g., control units and OSs in automobiles/airplanes/spacecrafts, air/railway traffic control systems, CPUs, cryptographic/communication protocols, medical machines. However, core techniques of formal methods have theoretical limitations (i.e., undecidability and computational difficulty) in general. So, we need to exercise ingenuity on reducing a real problem into solvable ones by using abstraction, approximation and relaxations, etc. and on combining multiple techniques to solve each of the reduced problems.
We tackle research on developing advanced techniques for expanding the scope of applications, and applying them to the development and verification of real products.

[Development of Basic Techniques]

We try to propose/extend basic techniques and algorithms for specification/development/verification of systems, to expand the scope of formal methods.

• Specification languages
  - Mathematical logics: propositional/predicate logic, (probabilistic/payoff) temporal logics [3]
  - Formal languages: omega-regular languages, domain specific languages [2]
• Verification/generation techniques
  - Program verification [2]
  - (Probabilistic/statistical) model checking
  - Specification verification
  　* Satisfiability (modulo theories) solving
  　* Realizability checking / optimal synthesis [3]
  - Test-case generation [1]

[Applications to Industrial Products]

We try to produce applicable formal methods by developing techniques and methods to bridge a gap between theories and practices through collaborative research with industry companies.

• Formal methods and verification tools for next-generation automotive system platforms (CREST project)
• Coverage test generation methods for Simulink models [1]
• Conformance checking methods for embedded software against cording standards / hardware manuals [2]
• Applications for digital transformation (DX)

Key publications

1. Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki: Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models, IEICE Trans. Fundamentals, Vol. E103-A, No. 02, pp. 451-461, 2020.
2. Thuy Nguyen, Takashi Tomita, Junpei Endo, Toshiaki Aoki: Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers, Software Testing Verification and Reliability, Vol. 31, Issue 8, e1788, 2021.
3. Takashi Tomita, Atsushi Ueno, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki: Safraless LTL Synthesis Considering Maximal Realizability, Acta Informatica, Vol. 54, Issue 7, pp. 655-692, 2017.

Equipment

Verification tools (model checkers, SAT/SMT solvers, etc.)
Modeling tools (MATLAB/Simulink, UML, etc.)