研究背景・目的

　近年、高い安全性の保証が必要なソフトウェアシステムが増加する一方、システム開発時に「そもそも対象システムはいかなるものか」の理解が曖昧なまま開発を進め、深刻な問題が発生することが増えています。これに対し、数学の言葉でシステムのモデルを作り望ましい性質を持つことを数学的に証明するアプローチがあります。本手法は強い保証と安全な理由の説明が得られるメリットがありますが、現代的なシステムに適用するには課題があります。まず対象システムそのものが非常に複雑であり、さらに、自動運転における時間遅延・計測誤差や、動作を書き下せない機械学習モジュールなど、各種の不確かさが存在します。私たちは、このようなシステムに対しても、厳密にモデルを構築・説明・検証するための手法を研究しています。

研究内容

　私たちは、段階的詳細化と呼ばれるモデル構築技法を応用して上記の問題に挑んでいます。段階的詳細化とは、先に対象の抽象的なスケッチを構築・証明し、後から対象の詳細を構築してスケッチと詳細の整合性を証明する、というプロセスを繰り返す技法です。それにより一気に作れない複雑な対象を、足元を固めながら段階的に構築・証明することができます。応用例として私たちは、計測誤差が発生するシステムについて、開発者が誤差をないものとして構築したシステムモデルを入力すると、自動で誤差があっても安全に動作するモデルに詳細化する手法を提案しました。構築した詳細モデルは許容できる誤差の限界を導くなどの分析にも使えます。

産業応用の可能性

　安全性について顧客や第三者に対する保証とその説明責任が求められるソフトウェアシステムが増えています。私たちの手法を用いると、システムのモデルとその安全性の根拠の厳密な構築を、より多くのシステムに対して行えます。例えば、計測誤差を扱う手法は、自動運転やドローンなど、実世界の環境の中で動く制御器システムについて回る「理想と現実の差」を引き受けます。これにより、開発者は誤差の細部に惑わされず制御の本質的な部分に集中できるほか、許容できる誤差の限界の分析を通じ、搭載可能なセンサに制約のあるシステムの構成を探索できます。また、数値誤差に限らず、物体認識システムの誤認識など、多様な環境と計測手段に対応する応用も期待できます。