背景・課題

時代はマルチコアの時代に入り、プログラムの性能向上のために、ソフトウェア技術者は部分部分が並列に動作するソフトウェアを開発せざるを得ない時代に突入しました。また、航空宇宙や医療、さらには車載のソフトウェアに関してはより安全なソフトウェアを確保するために機能安全規格などをクリアする必要性も高まっています。しかし、安全に動作する並列・分散プログラムの手法は未だ確立したとは言えない状況です。
PAT Pro(Process Analysis Toolkit Professional version)は、並列処理モデルとして歴史が長いCSP理論に基づいた並行プロセスモデルを採用しています。CSP(Communicating Sequential Process)は、Hoare博士が提案した並行プロセスを代数的に取り扱う事で、その複雑な振る舞いの安全性の証明や、二つの異なる表現のプロセスの等価性などを扱えます。その様な伝統的なCSPのモデルに対して近年注目されている「モデル検査」技術による挙動空間の網羅的な探索エンジンを備えています。

並行・分散システムまたは現状のモデル検査ツールには以下の様な課題があります。

リソース共有システムの複雑性

複数の並列に動作するプログラムが共通のリソースに対して書き込みを行うような状況で動作する場合、タイミングにまつわる様々な問題（「デッドロック」など）が増えています。これらの問題を「共有メモリ」を利用する事によって設計されたシステムを、レビューや限られたテストだけで検出、解決することは困難です。

モデル検査の敷居の高さ

形式手法の1分野である、モデル検査技術が注目されています。しかし、モデル検査は、「数理論理学」をベースにした非常に学術性の高い研究分野から発生した技術であるがゆえに、十分に利用するには利用者がその様な研究分野について学習する必要がありました。PAT ProがベースとしているCSPも、本来「プロセス代数」と呼ばれる非常に数学的な背景を持ったものであり、記述されたモデルの正当性などの検査には、数学的な証明テクニックを必要とします。

検証モデル記述言語の学習の負担

多くのモデル検査ツールによって検証される対象モデルはそのモデル検査ツールが独自に定義されたモデル記述言語で記述される必要があります（SPINのPromera等）。そのおかげで、モデル検査の利用に際しては、実際の開発プロセスの中で成果物として作成する設計書や、実装言語での記述とは別な言語を新たに習得するという負担があります。

解決策

PAT Proの利用によりそれらの問題を以下の様に解決します。

リソース共有システムの複雑性

リソースの共有問題を「共有メモリへの排他アクセス」という方法での解決に伴う困難性は、実際の設計者なら体験済みなのではないでしょうか？PAT ProがベースとしているCSP理論では、基本的にプロセス間通信を実現するのに「同期通信チャネル」を利用します。これはリソース共有システムに対しての有効な設計指針を示しており、今では並列処理を指向する様々な言語にこの機構（同期チャネル）が組み込まれつつあります。その様な設計指針で設計されたモデルを検査するのに最適なモデル検査ツールはPAT Proの様なCSPベースのモデル検査ツールとなります。

モデル検査の敷居の高さ

CSPでモデルの検証には本来数学的な証明テクニックが必要です。しかし、PAT Proは、モデル検査ツールなので、記述した対象モデルを検証するのにはSPINなどでも採用されている様な検証式を与える事で、後は自動で検証し、結果を出してくれます。

検証モデル記述言語の学習の負担

PAT Proでは、検査モデルの記述言語として、ベースになるCSPの他に複数の問題に特化した言語を用意しています。PAT Proの利用者はそれらから自分の問題に適した言語を選択して利用する事ができます。また、利用者の問題領域をより自然に記述てきるDSL(ドメイン特化型の言語）を理解し、検査できるように、PAT Proを拡張する事ができます。この様な事を実現するために、PAT Proではソフトウェアの構成を柔軟にしており、ユーザ自身が望む言語に対応する「モジュール」を開発する事によって、その要求をかなえる事ができます。