十年前の装置と、いまの装置を並べてみてください。違いは大きさではありません。関わっている人の数です。
機構、電気、制御、ソフト、安全。それぞれに担当がいて、それぞれが自分の範囲では正しいものを書いている。それでも立ち上げでは問題が出る。しかも、どの担当の資料を読み返しても、その問題は書かれていない。誰の設計にも書かれていない挙動が、組み上がった瞬間に現れる。
装置が、ひとりの頭に収まらなくなった。仕様書と実機が、どこかで静かにずれていく。この現象に見覚えのない装置エンジニアは、たぶんいません。
そして、これが起きたのは装置業界だけではありません。
世界はすでに、モデルで設計しはじめている
自動車も、航空機も、医療機器も、同じ壁にぶつかりました。出てきた答えは、設計を文書ではなくモデルで持つことでした。Model-Based Systems Engineering、Model-Based Design。呼び方はいくつかありますが、やっていることは同じです。要求も、状態も、インターフェースも、人が読む散文ではなく、機械が扱える構造として書く。
Simulink でブロック図を描くのも、SysML で状態機械を書くのも、設計管理ツールで要求とモジュールを紐づけるのも、全部この流れの中にあります。読んでいる方の会社でも、すでにどれかは動いているかもしれません —— そう呼んでいないだけで。
これは思いつきの話ではなく、市場として動いています。第三者調査による推計では、MBSE の市場規模は 2024 年に約 74 億ドル、2033 年には約 227 億ドル。年平均成長率にして約 13% です。「新しくて良さそうな考え方」の数字ではありません。すでに乗り換えが始まっていることの数字です。
つまり、この梯子には、多くの現場がもう足をかけています。
モデルは、つくるところまでしか面倒を見ない
ここで、モデリングツールが実際にやってくれることを並べてみます。
- モデルを書く場所を提供する
- モデルを図として見せる
- モデルの書式の整合性(参照漏れ、型の不一致)を確認する
- モデルからコードを生成する
最後のひとつは強力です。人が手で書き写す工程が消えるので、写し間違いという誤りの種類が、まるごとなくなります。
では、こう聞いてみてください。そのモデルは、正しいのですか。
どのツールも、この問いには答えていません。答えているように見えるものもありますが、見ているのは「モデルとして書式が整っているか」であって、「そのモデルの通りに装置を動かして安全か」ではない。
正しくないモデルからも、コードは完璧に生成されます。生成されたコードに誤りはひとつもない —— 書かれた通りに動く、という意味では。誤りはモデルの側にあり、コードをいくら読んでも出てきません。コードレビューでは絶対に見つからない誤りが、そこにあります。
モデルをつくることと、そのモデルが正しいと証明することは、別の仕事です。
別の仕事なので、別の道具が要ります。
空白を埋めるのが、形式手法です
ここまでを一本の梯子として並べると、こうなります。
装置が複雑になり、頭と紙のなかだけでは設計が追いつかなくなった
→ だから世界は「モデル」で設計するようになった(MBSE / MBD)
→ しかし「そのモデルは本当に正しいのか」は、誰も証明していない
→ 形式手法による検証が、その空白を埋める形式手法(formal methods)という名前は耳慣れないかもしれません。やることは単純です。設計に書いてある状態と遷移を数学的に扱える形に置き、起こりうる状態の組み合わせを機械に網羅させる。人が思いつかなかった順番も含めて、全部です。安全条件が破れる経路が一本でもあれば、それを見つけて返してきます。
大事なのは、これが梯子の一段上に乗る層だということです。横に並んで競合するものではありません。
先に、いちばん気になるところを潰しておきます。Simulink を捨てる必要はありません。 PLC のツールチェーンも、社内の設計管理も、品質マニュアルの手順も、そのままです。モデルはこれまで通りつくる。そのモデルに対して「両方の軸が同時に危険領域に入る手順は存在しないか」を問う工程が、コード生成の前に一段入る。それだけです。
入り口が、すでに手元にある設計成果物である —— ここが要点です。詳細設計には、装置がどういう状態を持ち、どういう順で動き、どの条件でインターロックが効くかが、もう書かれています。材料は足りています。
コード生成がうまくなるほど、設計が詰まる
いま、詳細設計を渡せばコードが出てくる、という状況が現実になりつつあります。装置業界がこれをどこまで受け入れるかは別の議論として、技術としてはそうなっています。
これは問題を消しません。移動させます。
設計が間違っていれば、AI はその間違った設計を、正確に実装します。手書きよりも速く、正確に、大量に。そして誤りはコードのどこにもありません —— 設計にあるからです。
コード生成が良くなるほど、設計がボトルネックになる。 工程の中でいちばん自動化されていない部分に、負荷が集まる。それだけの話です。ただ、その「それだけ」は、設計を確かめる手段を持っているかどうかで、まったく違う重さになります。
では、なぜ皆やっていないのか
ここは正直に書きます。この梯子は、上りやすくありません。
MBSE 自体、順調に普及しているわけではないのです。2024 年の INCOSE の調査は、導入の障壁として三つを挙げています —— 認知される複雑さ、既存の慣行との相性、学習曲線。
読んで分かる通り、どれも技術の話ではありません。「難しそうに見える」「いまのやり方と噛み合わない」「覚えるのに時間がかかる」。形式手法は、この三つの壁に、そっくり同じようにぶつかります。むしろ MBSE より強くぶつかる。数学の記法が出てきた時点で、多くの現場は手を止めます。それは怠慢ではなく、妥当な判断です。
だとすると、この一段を実際に上れるようにするために要るのは、理論の話ではありません。設計者が普段書いているものが、そのまま入り口になること。そして、結果が現場の言葉で返ってくること。ここが解けない限り、正しさの証明は論文の中に留まります。
DatumProof は、この一段を装置エンジニアが普段の設計成果物のまま踏めるようにすることを目的にした取り組みです。
次に読むもの
「設計を確かめる」といっても、それはテストとどう違うのか。ここが腑に落ちないと、話は前に進みません。テストと形式手法は、何が違うのかで扱います。
そして、こういう手法が実際に使われているのかどうか。答えは「使われている」で、しかも装置業界からそう遠くない場所です。誰が、実際に使っているのかで紹介します。