Towards Realization of Highly Safe and Reliable Systems
Associate Professor：TOMITA Takashi
formal methods, computer science, software engineering, digital transformation (DX)
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.
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 
- Formal languages: omega-regular languages, domain specific languages 
- Verification/generation techniques
- Program verification 
- (Probabilistic/statistical) model checking
- Specification verification
* Satisfiability (modulo theories) solving
* Realizability checking / optimal synthesis 
- Test-case generation 
[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.
- Coverage test generation methods for Simulink models 
- Conformance checking methods for embedded software against cording standards / hardware manuals 
- Applications for digital transformation (DX)
Prototype tool of test-case generation tool PROMPT
for Simulink models  (productized by a partner company)
- 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.
- 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.
- 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.
Verification tools (model checkers, SAT/SMT solvers, etc.)
Modeling tools (MATLAB/Simulink, UML, etc.)
I will teach you how to logically/abstractly/structurally think and discuss about a target problem. Through such thinking and discussions, you will learn how to identify the essence of the problem and how to find reasonable solutions.
You need to initiatively and continuously consider and decide goal/plan/tasks/approach/solutions of your research and study necessary knowledge and techniques for the solutions as an independent researcher (but I will present rough suggestions if necessary). I will give you advice on the directions of your consideration, decision and study via regular laboratory seminars.