形式証明はモデル検査の次

■モデル検査と形式証明
モデル検査と形式証明は形式検証技術の主要な技術である。

一般に、型式証明は「安全性証明」と言われているが、具体的に「安全性証明」というものは存在せず、「デッドロックがない」とか「ブレーキを踏むと必ずブレーキランプが点灯する」等の、様々な安全に関する性質を総称して安全性証明と呼んでいる。ですので、安全性証明ができた」と誰かが行っている時は注意をしたほうが良い。安全性など証明はできない。安全性に関する何らかの性質が示されてたのみである。「安全性証明ができた」という文言には誤解をさせるおそれがある。

ちなみに、「安全性証明」は形式証明とは同義ではない。安全性証明は型式証明によって示されるが、安全性証明は形式証明によってのみ示されるものではない。モデル検査によっても安全性証明は可能である。

さて、これら二つの技術を比較した際の大きな違いは自動か否か、及び、表現力の違いである。

形式検証では述語論理やHoare論理等の述語論理を基にした言語を用いてシステムや安全性の性質を記述可能である。そのため、記述表現力が高い。一方で、システムがその安全性に関する性質を満たすかを証明するのには自動では難しく、人間による手助けが必要である。これにより、対話的検証と呼ばれる。

モデル検査の特徴は自動検証である。システムと安全性に関する性質を与えると、ボタンひとつでシステムがその安全性の性質を満たすか否かを判定する。一方で、表現力は命題様相論理を含めた命題論理式に限られ、その表現力は型式証明でできるものよりも弱くなる。

■安全性に関する証明技術（形式証明、モデル検査）の産業移転を阻むものは何か？

システムの信頼性や安全性の重要性が認識される中、安全性に関する証明技術に対する世間の興味も少しずつではなるが増えているようである。

一方で、こうした世間の興味は10年前ほどからあるにも関わらず、こうした技術の産業化はあまり進んでいないように思える。まあモデル検査はまずまずであるが。。。

その理由は何か？その理由は学術的には、それぞれの立場からいろいろと言われている（ポジショントークとも言うべきでしょうか）。思いつくところでは以下の様な感じでしょうか。
・表現力が弱いから現場で使えない（形式証明の立場からは）
・自動検証はスケールしない（モデル検査の立場から）
・安全性の性質を抽出できない（他）

私の印象的には、その理由は、産業のほとんどでは仕様を形式的に書かないし、そんな時間もそんなコストもないからではないかと思う。

もっと言うと、産業のほとんどでは、仕様さえしっかり書いていないのではないか。

そんなところにモデル検査はまだしも、「形式証明」を持ち込むのにはギャップがありすぎて、いささか難しいような気がする。

■形式証明技術を技術移転する方法

（続く）