本文へジャンプ

Embedding Trustworthy Software into the Real World

ISHII Laboratory
Associate Professor:ISHII Daisuke

E-mail:
[Research areas]
Software Engineering (Formal Methods), Constraint Programming
[Keywords]
Cyber-Physical Systems, Embedded Systems, Model Checking, Program Verification, Interval Analysis

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 design/implement/verify next-gen safety-critical systems (e.g. automobiles and block chains). In the research activity, ability to capture the essential problem in a research topic and ability to propose properly a solution are developed. You are also trained to be able to implement a theory/technique in practice, from a perspective regarding the research/development trends and history. For each research topic, we aim at developing a software, while making it possible to demonstrate the idea against realistic examples. Furthermore, logical explanation skills are developed through publishing the research outcome.

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

Research outline

As a metaphor for computerized systems like automobiles and robots, we consider hybrid systems that behave both continuously and discretely. Our research is about reliable design, implementation and verification of hybrid systems. We are also doing research on numerical constraint programming technique, which enables describing hybrid systems with constraints (e.g. inequalities that involve reals) and solving the constraints in a reliable manner.

(1)Modeling, Simulation and Verification of Continuous-Discrete Hybrid Systems

We conduct research through developing various methods/tools for hybrid systems.
We study modeling languages that describe hybrid systems concisely and clearly. 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 encloses a behavior (i.e. trajectory) by a set of intervals together with uncertain values and numerical errors. We also study testing/verification methods based on the numerical simulators.


Simulation and verification of a hybrid system


A constraint satisfaction problem
(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 of the solver (e.g. to robotics) and a parallelization of the solver.

(3)Verification of Numerical Programs

To realize trustworthy tools such as simulators and solvers, we apply program verification. In this research, we actually 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. T. Yabu, D. Ishii. Machine-Aided Verification of Four Interval Arithmetic Operators. Proc. SCAN Conf., pp. 176–177, 2018.

Teaching policy

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.

[Website] URL:http://www.dsksh.com/ishii

PageTop