なぜ安全規格は、形式手法を求めるのか

「形式手法」という言葉を初めて聞いたとき、装置エンジニアの反応はだいたい同じです。

「数学の話でしょう。うちには関係ない」

無理もありません。記号が並び、証明という単語が出てきて、装置を動かしている人間の日常からは遠いところにある話に見えます。学会で発表される種類のもので、月曜日の朝に立ち上げる装置とは接点がない。そう読むのが自然です。

ただ、ひとつ引っかかることがあります。その「関係ない話」を、自社の棚に並んでいる安全規格のほうが名指しで挙げているという事実です。

規格は、すでに書いています

分野ごとに、こうなっています。

規格	領域	形式手法の位置づけ
IEC 61508	機能安全(一般)	最高安全等級 SIL 4 で形式手法を highly recommended
EN 50128	鉄道	SIL 3・4 で強く推奨
ISO 26262	自動車	推奨
DO-178C	航空	形式手法の適用指針 DO-333 を別途規定

一行ずつ読むと、推奨事項の一覧に見えます。並べて読むと、別のものが見えてきます。

機能安全の一般規格、鉄道、自動車、航空 —— 互いに独立に作られ、別々の委員会が、別々の事故の歴史を背負って書いたものです。その四つが、同じ技術に手を伸ばしている。

とくに DO-178C の行は、少し立ち止まる価値があります。航空は、形式手法に言及しただけではありません。どう適用するかを別冊にして書いた —— それが DO-333 です。

誰も使わないもののために、補足文書は書きません。適用指針が要るのは、実際に適用する人がいて、その適用の仕方で認証の可否が割れるからです。言及と別冊のあいだには、距離があります。

なぜ、独立に作られた規格が同じ結論に着いたのか

理由は、この連載でずっと書いてきた一文と同じです。

早期に発見するほど、後工程のコストが大幅に下がる。

規格が形式手法に行き着いたのは、それが理論として美しいからではありません。安全に関わる誤りを遅くに見つけることが、単純に割に合わないからです。現場で見つかれば再作業。量産で見つかればリコール。認証を通ったあとで見つかれば、再提出。

そしてもうひとつ。ある危険度を超えると、テストだけでは「その誤りは無い」と言い切れなくなります。

これは規格の作者が意地悪だからではありません。同時に動くものが増えるほど、起こり得る順序は組み合わせで増えます。ある水準から先は、全部試したと主張すること自体が物理的にできなくなる。SIL 4 とは、そこまで来てしまった、という意味です。

認証で問われているのは、バグの数ではありません

ここがいちばん大事なところだと思っています。

認証や品質監査でやっているのは、誤りを直すことだけではありません。評価者に対して、主張を立てることです。この装置は安全ですと言い、その根拠を示す。相手が見ているのは、根拠の質です。

二つの文を並べてみてください。

「テストしましたが、その事象は発生しませんでした」

「その状態には構造的に到達できないことを示しました」

日本語としては、似ています。中身は別物です。前者が示しているのは観測されなかったことです。後者が示しているのは存在しないことです。

「発生しませんでした」は観測の不在であり、「到達できません」は事象の不在です。両者の差は、試した回数では埋まりません。

評価者には、この差が分かります。客先の品質監査にも分かります。「何回テストしましたか」と聞かれている場面は、実のところ「あなたの主張はどちらですか」と聞かれている場面です。

難しい半分は、すでに終わっています

形式手法と聞くと、ゼロから新しい作業が増えるように聞こえます。ここは誤解です。

御社はすでに、リスクアセスメントをやっています。HAZOP をやり、危険事象を洗い出し、一覧にしている。安全要求仕様に落としている。認証のために、既にやっているはずです。

その一覧を、もう一度見てください。

二軸が同時に危険領域に入る
扉が開いた状態で搬送が動く
非常停止から、どうやっても復帰できない状態が残る

これは、書類のための書類ではありません。形式検証が入力として食べるもの、そのものです。危険シナリオの一つひとつが、「この状態に到達可能か」という問いにそのまま変換できます。そして到達不可能であることを示すのが、形式手法がやっていることです。

つまり、難しい半分は既に終わっています。何が危険かを知っているのは、規格でも道具でもありません。その装置を作っている人です。足りていないのは、その一覧を「起きませんでした」から「起こり得ません」に変える手段のほうです。

正直に書いておきます

ここまで読んで「うちも急がないと」と思った方がいたら、いったん止めてください。

あなたの装置は、たぶん SIL 4 ではありません。 DO-178C の下にもありません。一般的な工場自動化装置を作っているなら、いま形式手法を義務づけている規格は、ありません。この記事は、無い義務を有るように見せるために書いたものではありません。

では、規格の話は何のためにしたのか。

規格は、従うべき命令としてではなく、難しさがどこにあるかの信号として読む価値があります。四つの規格が独立に同じところへ手を伸ばした、という事実は、その技術についての情報です。それが自分に義務づけられているかどうかとは、別の情報です。

間違えることが許されなかった産業 —— 鉄道、航空、自動車の安全機構 —— は、コストを承知でここに手を伸ばしました。彼らが臆病だったからではありません。彼らのところでは、遅く見つけることの値段が先に露出しただけです。装置業界でその値段が安いわけではありません。請求書の届き方が違うだけです。

もうひとつ、実務的な観察を書いておきます。認証の圧力は、たいてい規制当局より先に、客先と輸出先から来ます。ある日、引き合いの仕様書に安全等級が書かれている。ある国に納めようとしたら、要求水準が違う。規制が変わるのを待っていると、その時点では既に遅い、という順序になりがちです。

いま義務ではない、は正しい。この先ずっと関係ない、はまた別の話です。

次に読むもの

規格が推奨しているのは分かった。では実際に使っているのは誰か —— 誰が、実際に使っているのかに、公開されている事例と、普及がどこまで進んでいないかを並べました。

「テストしました」と「示しました」の差が、技術として何なのか。それはテストと形式手法は、何が違うのかで扱います。