新しい手法の話を聞いたとき、装置業界の人間がまず知りたいのは効果ではありません。
「で、どこが使っているんですか」
この問いは、疑い深いから出てくるのではありません。装置は十年以上動きます。納めた先の生産ラインが止まれば、その責任は自分たちに返ってきます。実績のないものを客先の装置に載せられないというのは、慎重さではなく、業務上の当然の前提です。
なので、その問いに先に答えます。効果の話は、そのあとにします。
AWS は、2011年から使っています
Amazon Web Services は、2011年から実際の本番システムに TLA+ という形式手法を使っています。研究部門の実験ではありません。動いているサービスの設計に対して使い、社内では経営層が積極的に広めてきました。担当したエンジニア自身が「Use of Formal Methods at Amazon Web Services」という論文にまとめていて、これは TLA+ の作者である Lamport のサイトで公開されています。
なぜ彼らがそこまでやるのかは、装置屋には分かりやすい話です。AWS の商売は、分散システムが正しく動くことに全部乗っています。そして分散システムで高くつく誤りは、コードの書き間違いではありません。複数のものが同時に動いたときにだけ現れる、稀な順序です。
同時に動くもの。稀にしか現れない順序。テストで再現できない事象 —— 装置エンジニアが「たまに止まる」と呼んでいるものと、同じ種類の誤りです。
Airbus は、単体テストを置き換えられるかを調べています
Airbus は、形式手法が単体テストを置き換えられるかを検討しています。
この文の重さは、少し立ち止まる価値があります。彼らが調べているのは「テストの補助として使えるか」ではありません。「テストの代わりに立てられるか」です。航空機の単体テストは、やりたければやる作業ではなく、認証上やらなければならない作業です。それを別の手段で代替できるかを、真面目に検討対象にしている。
念のため書いておくと、これは検討段階の話であって、置き換えが完了したという話ではありません。ただ、検討の対象になり得るところまでは来ている、ということです。義務づけられた検証活動の代替候補として名前が挙がる手法は、そう多くありません。
CERN と GSI は、PLC の検証を「サービス」として出しました
装置業界にとって、いちばん近い前例はこれだと思います。
CERN と GSI は「Formal Verification of PLCs as a Service」という取り組みを公開しています。二か所、読むべきところがあります。
ひとつは PLC。Web サーバでも、航空機の制御計算機でもありません。工場の装置を動かしているのと同じ、産業用の制御機器です。形式手法がクラウドや航空の中でしか成立しない話なら、私たちには関係がありません。しかしこれは、産業制御そのものに当てられています。
もうひとつは as a Service —— 「サービスとして」の部分です。つまり、PLC を書いているチームの側に形式手法の専門家を置く、という前提を取っていません。専門家は外側にいて、検証だけが外から提供される。装置を作っている人は、装置を作り続ける。
社内に形式手法の専門家を一人雇って育てる、という話であれば、中堅の装置メーカにとっては現実的ではありません。外から検証を受け取る形なら、話が変わります。中堅の装置メーカが実際に買える形に、いちばん近い公開事例です。私たちが作ろうとしているのも、この形です。
三つの事例に、共通しているもの
クラウド基盤、航空機、加速器の制御。並べると、互いに何の関係もないように見えます。装置業界とも関係がないように見えます。
共通点はひとつです。どれも複数のものが同時に動くシステムで、どれも高くつく誤りがテストで再現できない側にあるということです。
だから彼らは、テストを厚くする方向ではなく、設計そのものを調べる方向に金を払いました。順序の組み合わせを人間が数え切れないことを、早い段階で認めたからです。
自動化装置は、この家族の一員です。軸があり、搬送があり、上位制御があり、インターロックがあり、それらが同時に動く。稀な順序で噛み合ったときだけ止まる。構造は同じです。ただ、まだそう言われていないだけです。
正直に書いておきます —— 普及は、していません
ここまで読むと、業界標準になりつつある技術の話に聞こえるかもしれません。そうではありません。
形式手法の産業界での採用は、いまも限定的でニッチです。これは反対派の評価ではありません。AWS 自身がそう述べています。十年以上使ってきた当事者が、広まってはいないと言っている。
では、効かないから広まらないのか。専門家 130人を対象にした調査では、採用の最大の障壁として **71.5% が「エンジニアの教育不足」**を挙げました。一位は「手法が有効かどうか疑わしい」ではありません。使える人がいない、です。
つまり、止まっている場所は技術の側ではなく、人の側です。
技術は実証済みです。普及は、まだです。
これが世界の実際の状態です。間違えることが許されない組織は、十年以上前から使ってきました。それ以外は、手をつけていません。「みんなやっています」でも「これが未来です」でもない。そのどちらでもない、という事実が、いま手元にある答えです。
だから「まだ普及していないから危ない」も、「もう業界標準だから急げ」も、どちらも状況の読み方としては間違っています。正しい読み方はこうです —— 効くことは既に分かっている。あとは、自分たちが使えるようになる道があるかどうかだけです。
そして CERN と GSI の事例が示しているのは、その道が「社内で専門家を育てる」しかないわけではない、ということです。
次に読むもの
形式手法を求めているのは、先進的な企業だけではありません。安全規格そのものが、条件付きでこれを要求しています。その事情は なぜ安全規格は、形式手法を求めるのか で扱います。
そもそも、なぜ装置ソフトウェアではテストに頼りきれないのか。その構造は なぜ装置ソフトウェアは、V字モデルの右半分を実行できないのか にあります。