本文へジャンプ

Towards Realization of Highly Safe and Reliable Systems


Senior Lecturer:TOMITA Takashi

E-mail:
[Research areas]
formal methods, computer science, software engineering,
[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.

  • Coverage test generation methods for Simulink models [1]
  • Conformance checking methods for embedded software against cording standards / hardware manuals [2]

Prototype tool of test-case generation for Simulink models [1] (productized by a partner company)

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, Toshiaki Aoki, Takashi Tomita, Junpei Endo: Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller, 26th Asia-Pacific Software Engineering Conference (APSEC 2019), pp. 86-93, 2019.
  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.)

Teaching policy

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.

PageTop