今、学び直す分散システムと様相論理 by チェシャ猫

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

みなさんは「ボタンをクリックすると機能 X が正しく動く」といったテストケースを目にしたことはありませんか？ お気づきの通り、このテストケースはあまり良くない例です。では、何が良くないのでしょう？ 一番の問題は、ここで言う「正しく」がどのような状態を指すのか、言い換えればこのテストケースが何を保証しているのか、が全く具体的ではない点です。

我々が何らかの方法でシステムの仕様を保証しようと考えた場合、テスト設計であるとか、あるいは自動化ツールのような、仕様を「テストする」ための方法論に目が行きがちです。しかしその前段階として、仕様を「記述する」というステップがあることは忘れてはいけません。入力に対して出力がある、いわゆる単体テストであればそれほど困らないかもしれません。しかし、例えば複数のサーバが協調して動く「分散システムの正しさ」だったら？ さらに、複数のサーバのうち一部が高負荷となってレスポンスを返したり返さなかったりする状況だったとしたら、全体の動作の「正しさ」にはどのような影響があるでしょうか？

自然言語による仕様の表現は、我々が普段なんとなくイメージしている以上の曖昧性を含みます。そしてその曖昧性を排してシステムに対するより良い理解と洞察を得るために、厳密な「共通言語」を定義したいという動機は、かなり旧い時代から現在に至るまで、一貫して計算機科学の興味の対象であり続けています。

本セッションでは、このような動機に応える様相論理とモデル検査について、可能な限り誤魔化さずに解説したいと思います。普段、分散システムを触っていて、何となく計算機科学の基礎が気になってきたぐらいの方にお薦めです。