Embedding Trustworthy Software into the Real World

Laboratory on Cyber-Physical Constraint Programming
Associate Professor：ISHII Daisuke

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

Skills and background we are looking for in prospective students

Although basic math and programming skills are preferred, it is fine to start learning specialized knowledge and skills after being assigned to the laboratory. Students 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 cyber-physical systems (CPSs), which are often safety critical. You will work on proposing original methods, implementing tools, and conducting experiments with the aim of software quality assurance in CPS. This will enable you to acquire the basic skills that will be useful in a wide range of CPS and software-related professions. Each student is encouraged to learn basic skills by conducting a whole research process, consisting of survey, problem formalization, system development, experimentation, publication of a paper, etc.

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

Research outline

Many real-world systems, such as self-driving cars, power plants and medical equipment, can be considered CPSs in which cyber components and physical components interact via sensors and actuators. We are researching methodologies and technologies based on the concept of “constraints” with the aim of building a safe and reliable CPS. Constraints are expressions of relationships in a specific domain, and examples include logical expressions with propositional variables, equation systems with real variables, and traffic rules with state variables of vehicles. We aim to describe these problems declaratively and logically, solve them efficiently, and explain them in a comprehensible way.

[Research Case 1] Modeling, Simulation and Verification of CPSs

Modeling. We study high-level modeling languages for CPSs (e.g. hybrid automata, temporal logic, and Simulink). We study their semantics, relationship between different languages/models, etc.
Simulation. In CPS development, numerical simulations of model behavior are useful, but defects caused by numerical errors and other factors can be an issue. We have been working on a method that computes a set of behaviors rigorously using interval analysis.
Verification. We are researching exhaustive testing and verification methods for CPS models and implementations. We are working on safety verification using constraint solvers (Ref. 1), improving verification efficiency through modularization (Ref. 2), and automatic test case generation, etc.
Application. We are participating in a project to apply the above techniques to the Autoware automated driving platform.

[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. The proposed solver is based on interval analysis, and it is possible to guarantee numerical accuracy of the results or to solve the problem while including uncertain values. We are also developing an SMT solver that can handle logic formulas with numerical variables precisely for CPS model checking (Ref. 3).

Key publications

1. D. Ishii, 他. SMT-Based Model Checking of Industrial Simulink, International Conference on Formal Engineering Methods (ICFEM), LNCS 13478, pp. 156-172, 2022.
2. D. Ishii. A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method, International Symposium on Model Checking Software (SPIN), LNCS 14624, pp. 67?84, 2024.
3. D. Ishii, T. Tomita, T. Aoki. Approximate Translation from Floating-Point to Real-Interval Arithmetic, NASA Formal Methods, LNCS 13260, pp. 733-751, 2022.