さまざまなシステムの保証に活用

　形式手法とは、ソフトウエアの品質を保証するために用いられている数学的、記号論理的手法である。NII の石川准教授は、形式手法の特徴を次のように説明する。

　「いまや、すべての構造物や工業製品に、数学が用いられています。例えば、ビルや橋梁を建設する場合には、地震や洪水といった自然災害などを考慮して構造計算を行い、最適な設計を行っています。ソフトウエアも同様に、品質や安全性を高めるために、数学を活用しています。ソフトウエアのふるまいが十分に定義されているか、不具合がないかを、数理論理学を用いて判断し、事前に不具合を修正し、正しく働くことを保証するのです」

　形式手法は、すでに多くの場面で利用されている。フランスの地下鉄では、高い信頼性を確保するために、形式手法を採用している。証明しながらプログラムを作る工程を経ることで、各部品の信頼性を高めることができたという。ほかにも、自動車向けのシステム開発やセキュリティなどへの応用があり、欧米主導による国際規格への適用も始まっている。

　また、形式手法によって品質を保証するというケースでは、次のような活用もある。米国では、トヨタが開発、製造、販売したクルマにおいて、アクセルペダルが戻らず急加速するという不具合が発生し、2009～2010年に大規模リコールを実施するに至った。このとき、NASAが形式手法などを用いて、これを検証。その結果、クルマのソフトウエア制御に関わる欠陥は見つからず、ソフトウエアが原因となった可能性については排除された。

　以上は品質保証のために強力な検証技術を活用した事例だが、そのほかにも形式手法は効果があるという。

　例えば、おサイフケータイで利用されているFeliCaの技術では、第2世代の開発において形式手法を採用し、構文・意味が決まった方式で厳密に仕様書を記述する形に変更。これによって、日本語や英語などの表記による曖昧な表現を排除することに成功した。社内外の開発者が、表現を正しく理解することで、仕様書に起因する問題が非常に少なくなった。以後の形式手法の利用法の改善もあり、記述不足や不明確な記述、記述の誤りにより後工程で問題が発生することはなくなったと報告されている。

複雑化するものづくりの安全保証に

　ここ数年、製造業において、形式手法に関心が集まっている背景にはいくつかの理由がある。
　一つめは、ものづくりの複雑さが増している点だ。クルマを例にあげれば、さまざまなエレクトロニクス機器やセンサーなどが搭載され、これらを一元的に制御することの難しさが開発者の頭を悩ませている。現在、1台のクルマに搭載されるセンサーは100個以上とも言われており、信頼性と安全性の確保、性能の維持といった要件の検証がますます難しくなっている。そこに、形式手法を用いることで、それらの要件をクリアしていくことができる。

　二つめは、メーカーに安全性保証と説明責任が求められていることである。最新のクルマには衝突防止機能が搭載されおり、この安全性を保証し、同時にその安全性について説明する責任が自動車メーカーには求められている。形式手法により自動検証を行い、安全性の保証と説明責任を果たすことができるようになるとして、関心が高まっているのだ。

　 そして、三つめが、新たな機能や応用が広がっていること。最たる例が自動運転だろう。自動運転中、クルマの前に人が飛び出して来た場合、どういう条件なら安全かを、形式手法を用いて計算することが可能になる。「形式手法を用いることで、個々のケースを一つずつシミュレーションするだけでなく、無数のケースを理論的にまとめて扱うような『強力な検証』も実現でき、自動運転の安全性を高めることができるのです」

　さらに、形式手法に人工知能（AI）を組み合わせることで、より効率的な検証が可能になり、品質向上にも役立つ。「クルマのような物理的な動きが加わると、複雑性は一気に増します。そこにAIを加えることで、問題の特性を学びながらある程度的を絞れるようになる。このような経験や傾向に基づくAIのアプローチを形式手法と組み合わせれば、これまでより効果的・効率的な検証が可能になるでしょう」と、石川准教授は語る。

品質向上と新たな技術へのチャレンジ

　このように、製造業を中心に、ソフトウエア工学的形式手法が注目を集めるなかで、石川准教授がリーダーを務める『蓮尾メタ数理システムデザインプロジェクト』のグループ3「インテリジェンス協働形式手法」は、どのような役割を果たすのだろうか。

　石川准教授は、「インテリジェンス協働というのは、人間やAIによる経験や傾向に基づくアプローチを従来の形式手法に交えていくということ」だと語る。

　「まずは、ますます複雑化する製造業のものづくりにおいて、ソフトウエア工学的形式手法がどのような効果を発揮するのか、産業界が何を求めているのかを探るところからスタートして、実務的視点からの学際的理論展開をめざします」

　具体的な取り組みの一つが、ものづくりの品質向上である。「これまでのものの作り方を検証するとともに、より効果的な作り方を模索するためのツールを提供します。これにより、完成したクルマが、単に安全なだけではなく、燃費が良く、速く走り、快適であるといったようなさまざまな条件を満たす際の、最適な品質を実現するものづくりの手法の検証が可能になります。また、効率的なものづくりという意味では、AIを組み合わせた形式手法を活用することで、一定の確信をもって信頼性保証を行うこともできます。例えば、従来、30種類の検証を行っていたものを、25種類で済むようにしたり、あるいは40種類に増やすべきといった判断ができたりするようになるでしょう」

　二つめは新たな技術への挑戦だ。ここでは、自動運転が直近のテーマになる。「目の前で起きていることを判断し、安全に自動運転を行うために、無数のケースを検討する必要があります。これを個々に人手でチェックするだけでなく、理論も踏まえてツールで検証し、安全性を保証するのです。ここでは、グループ2の「産業応用グループ」と連携して、同グループが取り組んでいる実際のクルマを利用した自動運転車による検証も行う予定です」

　こうした検証は、実際に、国内の自動車メーカーと連携しながら実施していくことなる。そして、ここで得た知見をクルマ以外の分野にも応用していく考えだ。

　もう一つ石川准教授が、今回の取り組みを通じて期待しているのが、異なる分野の専門家が交流することのメリットだ。

　今回のプロジェクトには、数理学、ソフトウエア科学、制御、人工知能など異なる分野の専門家が参画している。石川准教授がリードするグループ3では、民間企業も加わって、形式手法の活用に向けた技術追求や実験を行う。「プロジェクトを通じて、違う分野の専門家が一緒に論文を書くといったこともあるでしょう」と、これまでにない相乗効果に期待する。「とにかくやりたいことが多い。なにを優先するか、まず交通整理をしなければなりません」と、石川准教授はうれしさを隠さない。

　日本のものづくりを強化する上でも、このプロジェクトの成果に注目が集まる。

（取材・文＝大河原克行　写真＝佐藤祐介）