モデル検査の「モデル」とは

モデル検査の「モデル」とは何かを少し考えてみたい。というか考えるも何もモデル検査の開発者の一人Clarkeの文章を発見したので、それを報告するだけなのだけど。

まず、最近の一般的な理解は、どうもソフトウェアやハードウェアを単純化した「モデル」、ということであるらしい。例えば、Wikipediaには

モデル検査（Model Checking）とは、形式システムをアルゴリズム的に検証する手法である。ハードウェアやソフトウェアの設計から導出されたモデルが形式仕様を満足するかどうか検証する。仕様は時相論理の論理式の形式で記述することが多い。

とある。またPrinciple of Model Checking

 

には

Model-based verification techniques are based on models describing the possible system behavior in a mathematically precise and unambiguous manner... ...This provides the basis for a whole range of verification techniques ranging from an exhaustive exploration (model checking) to experiments with a restrictive set of scenarios in the model (simulation), or in reality (testing).

とあって、「モデル駆動テスト」などのモデルと同じ意味だとしているみたい。 まあ、モデル駆動開発のモデルはUMLだったりして数学的に厳密とは限らないから、この本の言っているモデルとはちょっと違うけど。

でもそれは私の認識とは違っていて、私の認識では、モデル検査の「モデル」は数理論理学の「モデル」から来ている。数理論理学では、論理式で表された言明や公理と、それを満たしたり満たさなかったりする構造の対を考えるのだけど、構造が言明を満たしている時、その構造はその言明の「モデル」という。

ただ、何を典拠にそういう認識を正当化したら良いか分からなかったところに、Clarkeの文章 The Birth of Model Checking を発見した。これによると、

The Model Checking problem is easy to state: Let M be a Kripke structure (i.e., state-transition graph). Let f be a formula of temporal logic (i.e., the speci cation). Find all states s of M such that M; s |= f. We used the term Model Checking because we wanted to determine if the temporal formula f was true in the Kripke structure M, i.e., whether the structure M was a model for the formula f.

ここで、モデル検査では時相論理式というもので仕様を書くわけだけど、それに対応する構造はKripke構造と言われる。システムの状態遷移は簡単にKripke構造と見なせるわけだけど、そうみなしたときあるシステムが与えられた時相論理式のモデルになっているかを判定するのがモデル検査、とClarkeは言っている。というわけで、私の認識は正しいことになると思う。Clarkeは引き続いてこうも言っている。

Some people believe erroneously that the use of the term "model" refers to the dictionary meaning of this word (e.g., a miniature representation of something or a pattern of something to be made) and indicates that we are dealing with an abstraction of the actual system under study.

というわけで、モデル検査の「モデル」を考えているシステムを単純化したもの、という見方はすくなくとも原義からは離れた見方だということになる。

ただ、モデル検査を売り込むとき、モデル駆動開発のモデルと（暗に）同一視させることが行われているような気がして、多分、元々の意味は忘れられて行くんでしょうね。