形式手法を用いた、Push通知の仕様検証

初めて投稿します。あも(@amoO_O)です。
「デッドロックが起こらないこと」
「『いつかは』期待した状態になること」
「『いつでも』期待しない状態にならないこと」
プログラミング上にバグが無くても、これらの問題は起こることがあります。それらは、そもそも仕様が間違っていたことに起因するバグですが、これを仕様策定の段階で見つけるのはとても困難ですね。何故なら仕様は、
・自然言語で共有される
・何度も変更される
・従って、曖昧な仕様が、曖昧なまま増えていく
からです。
仕様の正しさを担保するにはどうすればいいでしょう?
今回は、形式的な仕様記述と検証を行う技術、「形式手法」を紹介します。

形式手法について

形式手法とは、ソフトウェアやハードウェアシステムの仕様記述、検証をする技術です。
単体テスト、結合テスト、負荷テストなどは主に実際に開発したプログラムについて、プログラミング上の誤りが無いかをチェックするために行われます。
これに対し、形式手法を使った仕様検証は、そもそもシステムに矛盾が無いか、をチェックするために行われます。形式手法を使ってシステムに誤りが無い、ということを担保しながら開発を進めれば、手戻りが少なくなり、全体としての開発効率がアップすることが期待されます。

alloyについて

alloyはDaniel Jacson氏が開発した「モデル発見器」で、以下からインストールできます。
http://alloy.mit.edu/alloy
alloyは「非手続き型言語」の一つで、「アトム」と「関係」を使ってモデルを組み立てていきます。
アトム、関係に関するいくつかの論理式を入力すると、それらを満たすシステムモデルを見つけてくれます。
また、いくつかの論理式と検証したい論理式を入力すると、前者を見たし、後者を満たさない「反例」モデルを探してくれます。

形式手法の未来

形式手法自体は、新しい技術ではなく、1980年代頃からハードウェア、ファームウェア開発で使われてきました。
それが昨今のコンピューターの発展により、状態数が膨大になるソフトウェア開発でも適用できるようになりました。
しかしまだまだ、ソフトウェアの分野では発展の余地が残っています。
興味がありましたら、ぜひ勉強してみてください。



Fatal error: Allowed memory size of 268435456 bytes exhausted (tried to allocate 16271409 bytes) in /home/yumeco/www/prod/wp-includes/wp-db.php on line 1171