離散的なパラメータで制御される連続的な挙動を数学的に保証
形式手法がハイブリッドシステムの信頼性を高める

もしもソフトウェアのプログラムに潜むバグ（不具合）が、意図しない動作を引き起こしたらどうなるだろう。至るところでさまざまなソフトウェアが動いている現代社会においては、経済的な損失のみならず、人命に関わる重大な事故にもつながりうる。ソフトウェアからバグをなくすことは、社会や人の安全を保障する上で重要な課題だ。そこで、ソフトウェアの開発では、膨大なテストを行い、動作を検証する。しかし、すべてのケースを網羅することは不可能だ。効果的なテスト手法はあるものの、未発見のバグが内在する可能性を否定できない。一方、構築された仕様やプログラムを数学的に記述し、論理的に証明することで、どのような入力に対しても「プログラムが正しく動作する」ことを厳密に保証できれば、バグを見落とすことはない。このような厳密な検証手法は「形式手法」と呼ばれ、コンピュータの黎明期から研究されてきた。形式手法は、「未発見のバグが残る可能性のあるテスト検証の弱点を補完できる」として、ソフトウェア開発に近年利用されるようになった。末永幸平さんは、自動車の制御ソフトのように、現実の物体が関わるシステムにも形式手法を適用しようと研究を進めている。

末永さんは研究が目指すところを「例えば自動車はさまざまな部品の制御ソフトによって動作しますが、この自動車が実際に動く時、決して危うい状態にならないと厳密に保証したいのです」と説明する。例えばアクセルやブレーキの踏み込みに対する自動車の動きは離散的なパラメータで制御されるものの、実際の速度や進行方向など自動車の挙動は連続的だ。このように離散的な変数と連続的な変数を同時に扱う系をハイブリットシステムという。形式手法はこれまで離散的な状態を扱うソフトウェアの検証に用いられており、車のようなハイブリットシステムの検証に用いるのは難しい。「そこで私たちは、ゼロに限りなく近い微小な正の実数 “無限小”が、無限回ループされる概念を数学的に厳密に定義し、プログラムに取り入れました。この『超準プログラミング言語』を用いて、連続的変化を離散的変化として表現すると、従来の検証手法がそのままハイブリッドシステムに適用できたのです」と末永さん。超準プログラミング言語で表現された挙動を論理的形式に従って証明できれば、シミュレーションモデルのようにパラメータを変えてさまざまなパターンを検証しなくても、ソフトウェアが目的の性質（車が衝突しない、等）を満たしていることを保証できる。この新しい手法を実用化するため、末永さんは超準プログラミング言語に対する形式検証のアルゴリズムを備え、自動的に検証作業を処理できる検証ツールの開発にも取り組んでいる。「面白いことに、新たに開発した検証ツールでは、無限小の部分を任意の正の実数としても正常に検証できました。つまり理論的には、無限小が定義されていない一般的な言語にも適用できる可能性があります」と新たな発見を語る。既存技術との互換性が確保できれば、実用化に一段と弾みがつく。

さらに、末永さんは「さきがけ」プロジェクトで、先述のハイブリッドシステムを対象とした超準プログラム言語の検証ツールで用いたアルゴリズムを応用し、従来のソフトウェア検証ツールを高速化することに成功した。形式手法において検証の成否を分けるポイントとなるのが、不変条件^※の導出方法である。関係する変数を全て用いて導出した多項式など、テンプレートと呼ばれる論理式を定義して、ここから不定条件を導出する方法が主流だ。このため変数が多く複雑なソフトウェアプログラムでは、テンプレートがあまりに巨大になり、不変条件の導出処理が難しくなる。「ハイブリッドシステムに関する記述は変数も多く、不変条件の導出が困難でした。そこで、次元解析という手法を用いたアルゴリムによって、テンプレートの中でも意味のある部分だけ取り出すことで、テンプレートサイズを大幅に削減できました。これは既存の検証ツールにも使えるアルゴリズムです」と末永さん。数学的に正しさが保証された手法なので、テンプレートサイズを削減しても必要な不変条件を見逃すことはない。

予備実験では処理速度を10倍に高速化することに成功し、特許出願を行った。末永さんが「シナジー効果」と言う通り、ハイブリッドシステムを対象とした研究は、既存手法の改良にもつながり、形式手法をより強力な技術に発展させる。末永さんは研究の将来像を「ソフトウェア開発の現場で、技術者が日常的に自分のプログラムの正しさを確かめられる検証ツールを普及したい」と語る。学習のハードルは低いが安全性の度合いは高い、そんな開発環境やプログラミング言語の確立を目指した今後の研究に期待が高まる。