PostgreSQL + QueryCache

last update: 16 Dec 2005

5.1 プログラム検証

もともと、このプログラム検証がしたくて、題材としてPostgreSQL+QueryCacheを選んだようなもの。

データベースシステムにはACIDというシステムが満たすべき*明確な*特性が定義されているから、 プログラムの検証でもACIDを定式化できればよいと考えたわけだが、 QueryCacheの実装にかなり手間取ってしまった。

プログラム検証については、

Verification

ON-THE-FLY, LTL MODEL CHECKING with SPIN

このあたりも参照:

抽象化を用いた検証ツール

5.2 モデル化

プログラム検証のモデリングであるが、 今回は、ACID特性のうちのConsistentが満たされればよいわけで、 思いっきり単純化して、テーブルTABLEとキャッシュCACHEには1変数のみ保存できるとした。

只今、Spinと格闘中。

contents |index |previous

since 04/Oct/2004