ソフトウェアの高安全化・高信頼化を目指して

冨田研究室　TOMITA Laboratory
准教授：冨田 尭（TOMITA Takashi）

E-mail：
［研究分野］
形式手法、計算機科学、ソフトウェア工学、DX
［キーワード］
モデル検査、プログラム検証、仕様検証、モデル生成、プログラム生成、テスト生成

研究を始めるのに必要な知識・能力

基本的な数学知識、情報リテラシ、ITスキル及び論理的な思考能力を持っていることが必要です。また、研究テーマによっては、プログラミングスキルや計算理論、数理論理、確率・統計等の基礎知識を持っていることが望ましいです。

この研究で身につく能力

ソフトウェア/システムを分析・開発するための数学的な理論及び技術と、問題の本質を認識・整理するための抽象的・構造的な思考能力を身に付けることができます。また、そうした理論及び技術を組み合わせ（または必要に応じて拡張し）、問題を合理的に解決する手法を提案できるようになります。

研究内容

［形式手法］

　形式手法とは、数学を基盤とした言語・技術・ツールを用いてソフトウェア/ハードウェアの仕様記述・開発・検証を行う手法群です。
　数学を基盤としていることから安全性・信頼性を厳密に保証することができ、自動車・航空機・宇宙機の制御ユニットやOS、航空・鉄道管制系、CPU、暗号・通信プロトコル、医療機器などの高安全・高信頼が求められるシステムの開発・検証にしばしば適用されています。しかし、基盤技術に理論的限界（計算不能性や計算困難性）があるため、実践応用のためには抽象化・近似・緩和等の技法を利用することや複数技術を組み合わせることなど、様々な工夫が必要です。
　我々は形式手法の適用範囲を広げるための基礎技術開発や実製品の開発・検証への応用、他分野への応用の研究を行っています。

［基礎技術の開発］

　より広範に形式手法を適用できるように、システムの仕様記述・開発・検証の基礎技術/アルゴリズムの提案・拡張等を行っています。

• 仕様記述言語
  - 数理論理：命題/述語論理、（確率/利得）時相論理[3]
  - 形式言語：ω - 正規言語、領域特化言語[2]
• 検証技術/生成技術
  - プログラム検証：プログラムが仕様を満たすか検証[2]
  - モデル検査：システム/プログラムを抽象化したモデルが仕様を満たすかを検査
  　* 確率的/統計的モデル検査
  - 仕様検証：仕様に不備がないか検証
  　* 充足可能性（無矛盾性）判定
  　* 実現可能性判定/最適合成[3]
  - テスト自動生成：システムの機能/構造を動的検査するためのテストケース1式を自動生成[1]

［実製品の開発・検証への応用］

　企業との共同研究を通して、形式手法の理論と実応用の間のギャップを埋める技法・手法を開発し、産業界に展開可能な実践的な形式手法の確立を目指します。

• 次世代車載基盤システムのための形式手法と検証ツールの創出(CRESTプロジェクト)
• Simulinkモデルのカバレッジテスト自動生成技術の開発［1］
• 組込みソフトウェアのコーディング標準/ハードウェアマニュアルへの準拠性検査技術の開発［2］
• デジタルトランスフォーメーション（DX）への応用

製品化されたテスト自動生成ツールPROMPTのプロトタイプ[1]

主な研究業績

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, Takashi Tomita, Junpei Endo, Toshiaki Aoki: Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers, Software Testing Verification and Reliability, Vol. 31, Issue 8, e1788, 2021.
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.

使用装置

検証ツール（モデル検査器、SAT/SMT ソルバ等）
モデル化ツール（MATLAB/Simulink、UML等）