本記事ではCSPベースの「マルチドメイン・モデル検査ツール」である、PAT(Process Analysis Toolkit)について紹介する。モデル検査は、形式手法(Formal Method)という方法論を基礎とする技術であり、複雑さが増大しながらも安全性を求められる、現在のソフトウェア開発の状況に対する処方箋の１つとして注目されている手法である。
■開発者によるセミナーが開催
先日（2011/10/24)、NPO法人トップエスイー教育センターにて、NUS(シンガポール国立大学)のJin Song Dong准教授率いる研究チームにより開発された形式手法ツール「PAT(Process Analysis Toolkit)のチュートリアルが開催された。
http://topse.or.jp/docs/?q=node/30
■モデル検査ツールとは？
PATは、形式手法の応用ツールの中では「モデル検査ツール」というジャンルに分類される。
モデル検査ツールでは、主にシステムの挙動に関わるモデルを形式的な言語で記述する。その様に記述された挙動モデルが検証性質（例：ｘｘといった危険な状態に陥らない、等）を満たすかどうか、といった検証を行う。
以下の図はモデル検査ツールの一般的な構成と利用の流れである。
■PATの特徴
PATツールの特徴は以下の様なものである。
○PATのモデル記述言語はCSPである
CSP(Communicating Sequential Process)はTony Hoare(現Microsoft Research Fellow)教授が考案した数学的な理論の１つで、「プロセス代数」の一種である。本来「プロセス代数」では、代数式として表現された並行プロセスの性質を数学的な証明テクニックを駆使して「証明」する事で検証を進める。しかし、PATは、「モデル検査ツール」であるため、「定理証明」を行うための様々なテクニックをエンジニアに求めない。
○PATは統合システムである
PATで提供される基本的な３つの機能「モデル編集」「シミュレーション」「検査」は全て連動しているため、「統合環境」として機能する。
便利な「連動」としては、検査性質が満たされなかった場合に初期状態からそこまでの動作パス（反例と呼ばれる）をシミュレーションの画面で確認できる、といった事などがある。
以下はPATの３つの機能の画面の例である。
○DSL(Domain Specific Language)指向の形式手法
現在、モデル検査の利用者（潜在的なものも含む）は、様々な分野へと広がりを見せている。
その様なそれぞれのドメインを専門とする人にとって、モデル記述部分にはCSPの様な一般的な記述言語でなく、ドメイン特化型の専用言語(DSL)が使いたいと考えるであろう。PATでは、こういったDSLにより記述されたモデルを内部的にCSPモデルへ変換する事で、DSLでのモデル検査という方向を提案する。
現状、彼らが開発している(設計/実装/最適化中を含む）ドメイン特化型の記述言語としては以下の様なものがある。
-MDLモジュール：Stateflow(Matlab/Simulinkが採用している状態遷移モデル）
-NesCモジュール：NesC(センサーネットワーク記述言語）
-Orcモジュール：ORC(Orchestration記述言語）
-BPELモジュール：BPEL(Business Process記述言語/実装中)
尚、これらは現在配布されているバージョンには含まれていない。現在はCSPの拡張言語として比較的汎用的な記述言語(RTS,PCSP, PRTSモジュール）が標準で提供されている。
■マルチコア時代のモデル検査ツール
--------------------------------------------------------------------------
個人のPCが普通に２～８コアの「マルチコアプロセッサ」を搭載している時代に突入した。そんな状況の中で、これからのプログラマは、「複数のコアをいかに効率良く使うか」といった問題に直面する様になる。
意識的にプログラムを並列化し、複数のコアに処理を分担しないと今まで動いていたプログラムの性能が落ちてしまう事すら起こりうる。しかしながら、信頼おける並列処理ソフトウェアを作る方法論はまだ確立していない。
PATがベースとしているCSPは、元々が並列処理を基本とするプログラムの記述と検証のための理論である。そういった意味でPATがこれからのマルチコア上のプログラムを作成するプログラマの手助けをできる可能性は高い。
■ロードマップ
PATの進化は早い。はっきりした比較対象があるわけではないが、新バージョンリリースの情報が非常に頻繁に行われているため、その様な印象がある。実際、つい最近2011/10/20にVer.3.4がリリースされたが、2008/7/10日にリリースされた、Ver.1.2.0から、実に30回以上のリリースを繰り返しており、今後も非常に速いペースでの高速化、高機能化、そして、ツールとしての安定化が進んでゆくものと思われる。
「ロードマップ」として彼らが示しているものをいくつか紹介する
・新しいアプリケーションドメイン用モジュール
・パラメータ化された詳細化関係の検査
・確率的モデル検査
・UMLまたはFUMLの検査
・C#プログラムのモデル検査
・Promela言語⇒CSP#への変換
・State Chart⇒CSP#への変換
・VisualStudio/Eclipseとの統合
・PATモデルからC/C++の生成
■商用版
今後、PATは商用版（仮名PATPro)として形式手法ツールの販売ビジネスに入ってゆこうとしており、日本でも来年度までには正式に代理店を通した販売が開始しそうである（正確な次期は未定）。PATの主要開発メンバの３人は既に「Semantic Engineering Pte.Ltd.」という会社を設立し、その準備を進めている。
■学会発表など
PATの研究チームは近年行われている形式手法の関連学会への参加、発表を積極的に行っている。以下に、これまでに行われているものとこれから開催のものを一部紹介する。
-SSIRI2010(Secure Software Integration and Reliability Improvement)
PATの開発チームが所属するNUS(National University of Singapore)で開催。
オーガナイザはPATのチームリーダDr. Jin Song Dongであった。
-FM2011 (International Symbosium on Formal Method)
アイルランド・リムリック大学で開催。
Jin Songは大会最後のセッション「Model Checking」でチェアを務めた。
-ISSRE2011(International Symbosium on Software Reliability Engineering)
今年は、11月末から12月頭にかけて日本の広島にて開催される。
ISSR2011では、Jin Song以外の2名(Liu Yang, Jun Sun)がFormal Development and
Analysisというセッション(12/1 3:30pm～)にて、以下のテーマでPATに関する発表を行う。
PAT 3: AN EXTENSIBLE ARCHITECTURE FOR BUILDING MULTI-DOMAIN MODEL CHECKERS
ご興味のある方で参加可能な方は、貴重な機会なので是非参加しPATの可能性について直接感じとっていただければ幸いである。