普通の Web エンジニアのための様相論理入門 by チェシャ猫

本セッションでは、分散システムのような複雑な仕様や動作を持つプログラムに対して、様相論理を用いてその仕様を記述し検査する技術について解説します。

我々はシステムの仕様を保証する際、テスト設計や自動化ツールのような、仕様を「テストする」ための方法論を考えがちです。しかし、その前に仕様が「記述できる」ことが前提であり、これは決して自明ではありません。例えば、分散システムに対して「一部のサーバが落ちてもいつか回復する」といった性質なんて一体どうしたら表現できるのでしょうか？

複雑なシステムの仕様を考える上で、自然言語による曖昧性を排した「共通言語」を定義したいという動機は、古くから現在に至るまで、研究と実用が交わる大きなテーマの一つであり続けています。本セッションではこのような「共通言語」としての様相論理について、自分では手を出しづらいあなたのために、しかしできるだけ誤魔化さず解説します。