Embedding Trustworthy Software into the Real World
Associate Professor：ISHII Daisuke
Software Engineering/Science, Constraint Programming
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
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.
- D. Ishii, N. Yonezaki, A. Goldsztejn. Monitoring Temporal Properties using Interval Analysis. IEICE Trans. Fundamentals, E99-A(2):442–453, 2016.
- D. Ishii, A. Goldsztejn, C. Jermann. Interval-based projection method for under-constrained numerical systems. Constraints, 17(4):432–460, 2012.
- D. Ishii, T. Yabu. Computer-assisted Verification of Four Interval Arithmetic Operators. J. of Comp. and Applided Math., 377:1-13, 2020.
Each member of the laboratory is encouraged to learn basic skills by conducting a whole research process, which consists of e.g., survey, problem formalization, system development, experimentation, and publication of a paper. In a research, you will develop a method or a tool for some analyses on the target system (e.g. automobiles, robots and numerical programs). To accomplish the research, it is important to design and implement a system as well as to explain the system’s functions, behaviors, performance, properties, quality, etc. in a logical manner.