いま、大きいのはクラウドから小さいのはGPGPUまで、並行システムはなざかりです。
クラウドなど、並行システムが不可欠となったとき、並行システムのモデリング技法が必要になります。
でも並行システムを作るために使えるモデリング技法で、現場の技術者に定着したものはありません。
いま現場で使えるのは、オブジェクト指向モデリングです。
オブジェクト指向のモデリングではUMLを使うと思うのですが、UMLを使ったオブジェクト指向のモデリングでは、クラス図・オブジェクト図が静的な関係を表し、シーケンス図・コラボレーション図はシングルスレッドでのフローをあらわします。これらの図は静的な関係か、シングルスレッドをあらわします。
複数スレッドを扱えるのはアクティビティ図ですが、ここではスレッドの同期を扱えるだけです。
UMLでは、動的な関係の遷移を表すことができません。
並行システムを考えるときには、動的な関係の遷移を考えれる必要があるはずです。
オブジェクト指向は、述語論理と集合、オートマトンをベースにしていると思うのですが、これらには関係の時間遷移をあらわす能力がありません。
そこで、関係の時間遷移を扱える理論をベースにしたモデリング技術が必要になるはずです。今後数年の間に、こういったモデリング技術が提案されだすはずです。
クリプキ構造とか様相論理といった理論が重要になってくると思います。これらの理論は、並行システムのモデル検証に使われ始めているようです。
たぶん、このブログを読んでる人の多くは、物心ついたときからすでにオブジェクト指向モデリングがあったと思います。中には、UMLがすでに使われていたという人も多いかもしれません。
クラウドのような並行システムのモデリングは、これからです。
今後10年から15年くらいかけて、並行システムのモデリング技法が現れ淘汰され定着していく流れが見れるかもしれません。その過程では、並行システムを扱うことを主眼とした言語が脚光をあびるはずです。
そういった、パラダイムシフトのライフサイクルを最初から最後まで見れるのは、おもしろいかもしれません。
