形式手法 / Formal Methods

形式手法（Formal Methods）は、AmazonやMicrosoftがクラウドサービスの設計・検証に利用している技術で、システムを数学的な記法で表現します。要件定義書や設計書を数学的な記法で表すことで、自然言語による曖昧さを回避することや、システムが期待通り動くか、専用のツールで検証することができます。

今回は形式手法の１つ、FSP (Finite State Processes）という表記方法を紹介します。

例題：データベースシステム

この記事ではシンプルなデータベースシステムを設計することを例に説明します。このシステムは１つのプライマリーDBと、１つのセカンダリーDBからなり、書き込みはプライマリーDBに行い、読み込みはセカンダリーDBに行うシステムとします。プライマリーDBからセカンダリーDBへはデータがコピーされます。

FSP

準備：線形時相論理（Linear Temporal Logic、LTL）

なんだかむずかしいタイトルですが、自然言語を数学的に記述するのに利用します。下記の３つの表記方法をこの記事では使っています。

[] P: 常にPは真である。
<> P: 将来のいずれかの時点でPは真になる。
X P: 次の状態でPは真になる。

これを利用すると例えばデータベースシステムの性質を下記のように書くことができます。

プライマリーDBはいつも動いている: [] isRunning(primary)
セカンダリーDBはデータをもつ: <> hasData(secondary)
プライマリーDBに書き込みをされれば、セカンダリーDBにも書き込みがされる: [] (write(primary) -> <> write(secondary))
リクエストの後すぐにレスポンスする: [] (request(primary) -> X response(secondary))

ここでisRunning(x)、hasData(x)などは Predicate と呼ばれるもので、isRunning(x)はxが起動中であるときに真になり、hasData(x)はxがデータをもっているときに真になるとします。「->」は 内包(imply) と呼ばれるもので、「もし〜〜があったら」を表現するのによく使われます。

PredicateやImplyなどを詳しく知りたいという方がいらっしゃいましたら、下記のオンラインコースが参考になります。

FSP (Finite State Processes）

さて、本題の形式手法に入ります。形式手法ではたくさんの記述方法があるのですが、FSPは、教科書やツールがそろっており勉強の手始めに最適です。今回のデータベースシステムの例をFSPで記述すると下記のようになります。このコードは実際にLTSA Toolで動作するものであり、このツールを利用することで、状態遷移図を描画させたり、システムの検証をすることができます。

// プライマリーデータベースのモデル
// * 書き込みリクエストに対応する
PRIMARY = (request_write -> write_primary -> write_secondary
-> response_write -> PRIMARY).
// セカンダリーデータベースのモデル
// * プライマリーDBからの書き込みリクエストに対応する
// * 読み込みリクエストに対応する
SECONDARY = (request_read -> read_data -> response_read -> SECONDARY
|
write_secondary -> SECONDARY).

// システムはプライマリーDBとセカンダリーDBからなる
||SYSTEM = (PRIMARY || SECONDARY).

FSPコードは、イベントを順に記述していきます。プライマリーのほうは、request_writeイベントのあと、write_primaryイベントがあり、write_secondaryイベント、response_writeイベントを経て、また初期状態に戻ります。これは、クラアントからリクエストが来ると、まずはプライマリーDBに書き込み、その後セカンダリーDBに書き込んでから、クライアントにレスポンスを返すことを表現しています。セカンダリーのコードにある「|」という記号は２つのイベントのどちらかが起こることを示し、クライアントからの読み取りイベントrequest_readと、プライマリーからの書き込みイベントwrite_secondaryのどちらかを処理することを表現しています。

上記のコードをLTSA Toolで描画させるとそれぞれ下記のようになります。赤い丸で表現されている状態０が初期状態で、リクエストを待っている状態です。プライマリーDBに関しては、書き込みのリクエスト（request_write）が来ると、状態１に遷移します。このように、FSPでは状態に名前をつけるのではなく、状態を変化させるイベントに名前をつけるのが特徴です。セカンダリーDBの初期状態０は、読み込みのリクエスト（request_write）か、プライマリーDBからの書き込みリクエスト（write_secondary）を受け付けるものになっています。

モデルの検証

さてここからが面白いところで、FSPで記述されたデータベースシステムの検証を行っていきます。

最初に、「書き込みリクエストに対して、システムは最終的にレスポンスを返すかどうか」どうかを検証したいと思います。LTSA Toolに下記のコードを追記して、Compile後、「Check->LTL Property->GET_RESPONSE」と選びます。

// リクエストが来た状態とレスポンスを返した状態を定義
fluent W_REQUEST = <{request_write}, {response_write, write_primary, write_secondary}>
fluent W_RESPONSE = <{response_write}, {request_write, write_primary, write_secondary}>

// リクエストが来た場合、最終的にはレスポンスを返すことを検証
assert GET_RESPONSE = [](W_REQUEST -> <>W_RESPONSE)

LTSA Toolが総当りで検証した後、「No LTL Property violations detected.」と表示され、このモデルではリクエストが来たら、そのうちレスポンスを返す性質を保証していることがわかりました。

では、違反する例を見てみましょう。下記のコードでは、プライマリーの書き込みのすぐ後、セカンダリーへ書き込む性質があるかどうか調べます。

// プライマリーへの書き込みの状態とセカンダリーへの書き込みの状態を定義
fluent W_PRIMARY = <{write_primary}, {request_write, write_secondary, response_write}>
fluent W_SECONDARY = <{write_secondary}, {request_write, write_primary, response_write}>

// プライマリーの書き込みの次の処理は必ずセカンダリーへ書き込みを行うことを検証
assert DOUBLE_WRITE = [](W_PRIMARY ->X W_SECONDARY)

同じように検証を行うと今度は、「Trace to property violation in DOUBLE_WRITE:」と出て、今回の仕様では、プライマリーの書き込み直後にセカンダリーへの書き込みが行われない場合があることを指摘しています。エラーメッセージにはトレース（Trace）という、違反するまでに辿ったイベントが記載されているので、これを参考に仕様上のバグを見つけることができます。今回のシステムでは、プライマリーにデータが書かれた後、セカンダリーにデータが書かれる前に、セカンダリーは読み込みリクエストに対応できるのが違反の理由でした。

まとめ

今回は形式手法の１つFSPを紹介しました。プログラミング言語とは異なる表記方法ですが、わりと直感的に書けるのと、小さいシステムであれば状態遷移図を描画させることができるので形式手法を学ぶ目的でもFSPがおすすめです。

最終的に、3つのイベントを経て見つかる簡単な仕様上のバグ（プライマリーの書き込み直後にセカンダリーへ書き込みされない）を検出しましたが、Amazon DynamoDBの場合は最低でも35イベント[1]を経ないと見つからないバグだったそうです。再現するのにそれだけ多くのイベントを必要とするバグの検出は、人間の頭では難しく、AmazonはTLA+という別の形式手法で、AWSの設計、検証を行っているそうです。

もし、もっと知りたいという方がいらっしゃいましたら、下記の本をおすすめします。

Concurrency: State Models and Java Programs

引用

How Amazon Web Services Uses Formal Methods