Embedding Trustworthy Software into the Real World

ISHII Laboratory
Associate Professor：ISHII Daisuke

E-mail：
［Research areas］
Software Engineering/Science, Constraint Programming
［Keywords］
Embedded Systems, Autonomous CPS, Model Checking, Program Verification, Reliable Simulation

Skills and background we are looking for in prospective students

Basic knowledge of mathematics, programming skills and technical survey skills are preferred. Students with logical interaction skills (between persons) who will strive for a research goal are most welcome.

What you can expect to learn in this laboratory

You will learn theories and techniques to model/design/implement/verify safety-critical systems (e.g. autonomous vehicles and block chains). In studying a theory/technique, you propose a novel method, implement a software tool, and/or conduct experiments on a computer. In the research activity, (1) ability to capture the essential problem and to propose properly a solution, (2) perspective regarding the research/development trends and history, and (3) logical explanation skills in publishing the research outcome will be developed.

【Job category of graduates】 Software industry, manufacturing industry, startups

Research outline

Aiming at trustworthy real-world systems, we adopt an approach that considers “constraints” as an intermediate language. To realize a system from an idea and requirements, (i) we model and design the system using high-level models and/or logical/mathematical formulas, and (ii) apply e.g. search-based solving, numerical simulation, and static analyses to them. These results will contribute to the implementation and verification of the target system. We also plan to apply the approach to autonomous systems whose components are generated by machine learning.

[Research Case 1] Modeling, Simulation and Verification of Continuous-Discrete Hybrid Systems

We study high-level modeling languages for hybrid systems consisting of cyber and physical modules. Herein, we consider formal languages (e.g. hybrid automata and temporal logic), and practical languages (e.g. Simulink), and study their semantics, relationship between different languages/models, etc.
Given a model, it is important to simulate its behavior and test/verify behaviors exhaustively. We have been working on a simulation method that analyzes a set of behaviors (i.e. trajectories) using interval analysis. We also study testing/verification methods based on the numerical simulators.

[Research Case 2] Numerical Constraint Programming

We have been developing a constraint solver for satisfiability/optimization problems described by a set of constraints that involve real variables. To build an efficient solver, we exploit various search and numerical techniques. The proposed solving process is based on interval analysis methods for certifying the precision of a result and computing with uncertainties. We also work on applications (e.g. robotics) and parallelization of the solver.

[Research Case 3] Verification of Numerical Programs

To realize trustworthy tools such as simulators and solvers, we conduct program verification. We construct programs that involve floating-point computations and complex structures, while proving their correctness using SMT solvers and proof assistants.

Key publications

1. D. Ishii, N. Yonezaki, A. Goldsztejn. Monitoring Temporal Properties using Interval Analysis. IEICE Trans. Fundamentals, E99-A(2):442–453, 2016.
2. D. Ishii, A. Goldsztejn, C. Jermann. Interval-based projection method for under-constrained numerical systems. Constraints, 17(4):432–460, 2012.
3. D. Ishii, T. Yabu. Computer-assisted Verification of Four Interval Arithmetic Operators. J. of Comp. and Applided Math., 377:1-13, 2020.