自動運転に欠かせない「バグのない制御ソフトを開発する」(2)　形式手法とは?

　ソフト開発においてはバグのないことが絶対的に求められている。だが、現状の日本の法律の立て付では、自分のクルマにバグがあった場合に「運が悪い人」で終わってしまう。その中で、「数理論理学」でバグがないことを証明できないかとの取り組みが続いている。数学の定理証明によって欠陥がないことを証明できるとみて開発が進められてきているのだ。

【前回は】自動運転に欠かせない「バグのない制御ソフトを開発する」(1) バグは必ずある

　まず、システム設計の段階で「論理的矛盾がないのか？」を検証する。この段階での検証は、これまでの「力仕事」の開発現場では十分に行われてきてはいない。コーディングが終わってからのテストが主であるのが現実だ。

　昔遭遇したBMWの欠陥では、センサーが異常を感知した場合に、「システムダウン」と決められた処理が行われていた。そのため、「エンジンを止めては危険な場面」、つまり走行中でもエンジンをストップさせてしまうのだ。踏切の中でも、200km/hで巡行中でも「エンスト」する事態となっていた。

　これはシステム設計の段階において、エラー処理の手段を的確に選別する処理を行わず、システム設計の下位に当たる展開で、プログラム仕様書で部位によって処理の仕方を変えていないために起こっている現象だった。

　そのためすぐには修正が難しく、システムの変更に戻ってからコーディングの変更をしなければならない必要があった。しかも、その部品はボッシュ（メガサプライヤー）の製品で、メーカーであるBMWの支配下にはなく、欧米のメーカーの常として修正には証拠を突きつけなければならなかったのだ。

　一方、日本のPL法（製造者責任法）では、データを持たない被害者側が証明しなければならず、事実上、所有車の修理が不可能だった。このような状況のままだと、自動運転時代の社会の要請にはこたえられるはずもない。

　こうした「システム開発段階のそれぞれのレベルでの横の展開」と、「それをコーディングレベルまで具体化していくときの縦の展開」の関係も考慮した「形式手法」のような数理論手法を使った検証システムが開発されてきている。

　これまでは、完成したシステム段階での検証は不可能に近いほどのデータ量だったのだ。それがAIによって可能となってきている。確かにプログラムのテストにAIを使うことは当然であり、論理的矛盾を見つけ出すことはかなりの確率で出来るはずだ。数理論検証でなくてもある程度の時間をかければ、AIならば予測されるデータ全ケースについて試すことが出来るかもしれない。

　コーディング前に「形式手法」によって論理的矛盾を検証できるのであれば、素早い対応が可能となるので開発コストも削減できるはずだ。実務においては「形式手法」で検証するのも「力仕事」になってしまうので、AIを使うことが前提となろう。

　その昔、大したシステムではないが、バッチシステムなのにオンラインリアルタイムのようにシステムを組んだSEがいた。そのシステムを、すべてのケースに渡ってデータを想定するように私はデバッグしたのだが、昔はコーディング前にテストするには「机上デバッグ」しかないので、頭を抱えて行っていたら先輩たちに「入り口と出口のデータだけでいいんだよ！」と笑われてしまった。

　それほど、バグのないシステムなど考えられなかったのだ。ソフト開発においては、「ほぼ良し」で実用化されているのが現実だ。この問題を何とか出来る可能性が、数理論理学など「形式手法」にはあるのだ。

続きは:自動運転に欠かせない「バグのない制御ソフトを開発する」（3）　完璧な論理などありえない（記事：kenzoogata・記事一覧を見る）