分散プロセスの構築と分析

分散プロセスの構築と分析

開発者	INRIA CONVECS チーム (旧 VASY チーム)
初回リリース	1989年、34～35年前
安定リリース	2023年 / 2023年2月13日; 21か月前 ( 2023-02-13 )
オペレーティング·システム	Windows、macOS、Linux、Solaris、OpenIndiana
タイプ	通信プロトコルと分散システムを設計するためのツールボックス
Webサイト	cadp.inria.fr

CADP ^[1] (分散プロセスの構築と分析) は、通信プロトコルと分散システムを設計するためのツールボックスです。CADPは、INRIA Rhone-AlpesのCONVECSチーム (以前はVASYチーム) によって開発され、さまざまな補完ツールに接続されています。CADPはメンテナンスされ、定期的に改善され、多くの産業プロジェクトで使用されています。

CADP ツールキットの目的は、シミュレーション、迅速なアプリケーション開発、検証、およびテスト生成 のためのソフトウェア ツールとともに形式記述技術を使用することで、信頼性の高いシステムの設計を容易にすることです。

CADP は、非同期並行性を備えたあらゆるシステム、つまり、インターリーブ セマンティクスによって制御される一連の並列プロセスとして動作をモデル化できるあらゆるシステムに適用できます。したがって、CADP は、ハードウェア アーキテクチャ、分散アルゴリズム、通信プロトコルなどの設計に使用できます。CADP に実装されている列挙検証 (明示的状態検証とも呼ばれる) 手法は、定理証明ほど汎用的ではありませんが、複雑なシステムの設計エラーを自動的かつコスト効率よく検出できます。

CADP には、信頼性の高いシステム設計に必要な形式手法における 2 つのアプローチの使用をサポートするツールが含まれています。

• モデルは、並列プログラムおよび関連する検証問題の数学的表現を提供します。モデルの例としては、オートマトン、通信オートマトン ネットワーク、ペトリ ネット、二分決定図、ブール方程式システムなどがあります。理論的な観点から、モデルの研究では、特定の記述言語に依存しない一般的な結果を求めています。
• 実際には、モデルは複雑なシステムを直接記述するにはあまりにも初歩的すぎることがよくあります (これは面倒でエラーが発生しやすいためです)。このタスクには、プロセス代数またはプロセス計算と呼ばれるより高レベルの形式化と、高レベルの記述を検証アルゴリズムに適したモデルに変換するコンパイラが必要です。

CADP の作業は 1986 年に始まり、最初の 2 つのツールである CAESAR と ALDEBARAN の開発が着手されました。1989 年に CADP という頭字語が作られました。これはCAESAR/ALDEBARAN Distribution Packageの略です。時間が経つにつれて、ツールの提供を可能にするプログラミング インターフェイスなど、いくつかのツールが追加されました。CADP の頭字語はその後CAESAR/ALDEBARAN Development Packageになりました。現在、CADP には 50 を超えるツールが含まれています。頭字語は同じままですが、ツールボックスの名前は、その目的をよりよく示すために、 Construction and Analysis of Distributed Processesに変更されました 。

CADP のリリースには、アルファベット (「A」から「Z」) で順次命名され、その後、LOTOS言語に積極的に取り組んでいる学術研究グループが所在する都市の名前、さらに一般的には、並行性理論に大きな貢献をした都市の名前が付けられました。

メジャー リリースの間には、マイナー リリースが頻繁にリリースされ、新機能や改善点への早期アクセスが提供されます。詳細については、CADP Web サイトの変更リスト ページを参照してください。

CADP は、ステップバイステップのシミュレーションから大規模な並列モデルチェックまで、幅広い機能を提供します。これには以下が含まれます。

• いくつかの入力形式用のコンパイラ:
  • ISO言語LOTOSで記述された高水準プロトコル記述。^[2]ツールボックスには、シミュレーション、検証、テストの目的でLOTOS記述をCコードに変換する2つのコンパイラ（CAESARとCAESAR.ADT）が含まれています。
  • 有限状態マシンとして指定された低レベルのプロトコル記述。
  • 通信するオートマトン、つまり並列に実行され同期された有限状態マシン (プロセス代数演算子または同期ベクトルを使用) のネットワーク。
• BCG_MIN や BISIMULATOR などのいくつかの同等性チェックツール (双模倣関係を法とする最小化および比較)。
• EVALUATOR や XTL など、さまざまな時相論理とミュー計算用のモデル チェッカーがいくつか。
• 複数の検証アルゴリズムを組み合わせたもの: 列挙検証、オンザフライ検証、二分決定図を使用したシンボリック検証、合成最小化、部分順序、分散モデルチェックなど。
• さらに、視覚的なチェック、パフォーマンス評価などの高度な機能を備えたその他のツールも用意されています。

CADP はモジュール方式で設計されており、中間形式とプログラミング インターフェイス (BCG や OPEN/CAESAR ソフトウェア環境など) に重点を置いています。これにより、CADP ツールを他のツールと組み合わせたり、さまざまな仕様言語に適応させたりすることができます。

検証とは、複雑なシステムを、システムの意図された機能の特性を表す一連のプロパティ (デッドロックの回避、相互排除、公平性など) と比較することです。

CADP の検証アルゴリズムのほとんどは、ラベル付き遷移システム (または、単にオートマトンまたはグラフ) モデルに基づいています。このモデルは、一連の状態、初期状態、および状態間の遷移関係で構成されます。このモデルは、多くの場合、調査対象のシステムの高レベルの記述から自動的に生成され、さまざまな決定手順を使用してシステム プロパティと比較されます。プロパティを表現するために使用される形式に応じて、2 つのアプローチが可能です。

• 動作プロパティは、システムの意図された機能をオートマトン（またはオートマトンに変換されるより高レベルの記述）の形式で表現します。このような場合、検証への自然なアプローチは等価性チェックであり、これは、システム モデルとそのプロパティ（両方ともオートマトンとして表現される）を何らかの等価性または事前順序関係を法として比較することです。 CADP には、さまざまな等価性および事前順序関係を法としてオートマトンを比較して最小化する等価性チェック ツールが含まれています。これらのツールの一部は、確率モデル（マルコフ連鎖など）にも適用されます。 CADP には、システムのグラフィカル表現を検証するために使用できる視覚チェック ツールも含まれています。
• 論理プロパティは、システムの意図された機能を時相論理式の形式で表現します。このような場合、検証の自然なアプローチはモデル検査であり、これはシステム モデルが論理プロパティを満たしているかどうかを判断することです。CADP には、強力な時相論理形式である様相 mu 計算用のモデル検査ツールが含まれています。様相 mu 計算は、モデルに含まれるデータに対する述語を表現できるように、型付き変数と式で拡張されています。この拡張により、標準の mu 計算では表現できないプロパティ (たとえば、特定の変数の値がどの実行パスでも常に増加するという事実) が提供されます。

これらの技術は効率的で自動化されていますが、モデルが大きすぎてコンピュータのメモリに収まらない場合に発生する状態爆発問題が主な制限となります。CADP は、2 つの補完的な方法でモデルを処理するソフトウェア テクノロジを提供します。

• 小さなモデルは、そのすべての状態と遷移をメモリに保存することで明示的に表現できます (徹底的な検証)。
• より大きなモデルは、検証に必要なモデルの状態と遷移のみを探索することによって暗黙的に表現されます (オンザフライ検証)。

信頼性が高く複雑なシステムを正確に仕様化するには、実行可能 (列挙検証用) かつ形式意味論 (設計者と実装者の間で解釈の相違につながる可能性のある言語としての曖昧さを回避するため) を備えた言語が必要です。形式意味論は、無限システムの正しさを確立する必要がある場合にも必要です。これは、有限の抽象化のみを扱う列挙手法では実行できないため、形式意味論を備えた言語にのみ適用される定理証明手法を使用して実行する必要があります。

CADP は、システムのLOTOS記述に基づいて動作します。LOTOS は、プロトコル記述の国際標準 (ISO/IEC 標準 8807:1989) であり、プロセス代数 (特にCCSとCSP)の概念と代数抽象データ型を組み合わせています。したがって、LOTOS は非同期の並行プロセスと複雑なデータ構造の両方を記述できます。

LOTOS は 2001 年に大幅に改訂され、E-LOTOS (Enhanced-Lotos、ISO/IEC 標準 15437:2001) が公開されました。これは、より優れた表現力 (たとえば、リアルタイム制約のあるシステムを記述するために定量的な時間を導入するなど) と、より優れたユーザー フレンドリさを提供することを目指しています。

他のプロセス計算または中間形式の記述を LOTOS に変換し、CADP ツールを検証に使用できるツールがいくつか存在します。

CADP は大学や公的研究機関に無料で配布されています。産業界のユーザーは、非商用目的での評価ライセンスを一定期間取得できますが、その後はフルライセンスが必要となります。CADP のコピーをリクエストするには、登録フォームに記入してください。^[3] ライセンス契約に署名すると、CADP のダウンロードとインストール方法の詳細が届きます。

ツールボックスにはいくつかのツールが含まれています:

• CAESAR.ADT ^[4]は、LOTOS抽象データ型をC型とC関数に変換するコンパイラです。この変換には、パターンマッチングコンパイル技術と、最適に実装された通常の型（整数、列挙型、タプルなど）の自動認識が含まれます。
• CAESAR ^[5]は、 LOTOSプロセスをCコード（ラピッドプロトタイピングとテスト用）または有限グラフ（検証用）に変換するコンパイラです。変換はいくつかの中間ステップを使用して行われ、その中には、型付き変数、データ処理機能、およびアトミック遷移で拡張されたペトリネットの構築が含まれます。
• OPEN/CAESAR ^{[6] は}、グラフをオンザフライで探索するツール（シミュレーション、検証、テスト生成ツールなど）を開発するための汎用ソフトウェア環境です。このようなツールは、特定の高級言語に依存せずに開発できます。この点で、OPEN/CAESAR は、言語指向のツールとモデル指向のツールを結び付けることにより、CADP において中心的な役割を果たします。OPEN/CAESAR は、次のようなプログラミング インターフェイスを備えた 16 個のコード ライブラリのセットで構成されています。
  • いくつかのハッシュ関数を含むCaesar_Hash
  • Caesar_Solve はブール方程式を即座に解く
  • Caesar_Stack は深さ優先探索のためのスタックを実装します。
  • 状態、遷移、ラベルなどのテーブルを処理する Caesar_Table。

OPEN/CAESAR 環境内では、次のようなさまざまなツールが開発されています。

• • BISIMULATORは、双シミュレーション同値性と順序をチェックします。
  • オンザフライ定常状態シミュレーションを実行するCUNCTATOR
  • DETERMINATOR は、通常、確率、または確率的システムにおける確率的非決定性を排除します。
  • DISTRIBUTORは複数のマシンを使用して到達可能な状態のグラフを生成します
  • EVALUATORは、通常の交替のないμ計算式を評価する。
  • コードのランダム実行を行うEXECUTOR
  • EXHIBITORは、指定された正規表現に一致する実行シーケンスを検索します。
  • 到達可能な状態のグラフを構築するジェネレータ
  • 到達可能性分析の実現可能性を予測するPREDICTOR
  • PROJECTORは通信システムの抽象化を計算する
  • REDUCTORは、さまざまな同値関係を法として到達可能な状態のグラフを構築し、最小化する。
  • インタラクティブなシミュレーションを可能にするSIMULATOR、X-SIMULATOR、OCIS
  • デッドロック状態を検索するTERMINATOR
• BCG (バイナリ コード グラフ) は、非常に大きなグラフをディスクに保存するためのファイル形式 (効率的な圧縮技術を使用) であると同時に、分散処理用にグラフを分割するなど、この形式を処理するためのソフトウェア環境でもあります。多くのツールが入出力にこの形式を使用しているため、BCG は CADP でも重要な役割を果たします。BCG 環境は、プログラミング インターフェイスを備えたさまざまなライブラリと、次のようないくつかのツールで構成されています。
  • BCG_DRAWはグラフの2次元ビューを構築します。
  • BCG_EDIT は、Bcg_Draw によって生成されたグラフレイアウトを対話的に変更できるようにします。
  • BCG_GRAPHは、実用的に役立つさまざまな形式のグラフを生成します。
  • BCG_INFOはグラフに関するさまざまな統計情報を表示します
  • BCG_IOはBCGと他の多くのグラフ形式間の変換を実行します。
  • BCG_LABELSは、グラフの遷移ラベルを非表示にしたり、（正規表現を使用して）名前を変更したりします。
  • BCG_MERGEは、分散グラフ構築から得られたグラフフラグメントを収集します。
  • BCG_MIN は、強い同値性または分岐同値性に基づいてグラフを最小化します (確率的および確率的システムも処理できます)
  • BCG_STEADYは、（拡張）連続時間マルコフ連鎖の定常数値解析を実行します。
  • BCG_TRANSIENTは、（拡張）連続時間マルコフ連鎖の過渡数値解析を実行します。
  • PBG_CPは分割されたBCGグラフをコピーする
  • PBG_INFOは、分割されたBCGグラフに関する情報を表示します。
  • 分割されたBCGグラフを移動するPBG_MV
  • PBG_RMは分割されたBCGグラフを削除します。
  • XTL (eXecutable Temporal Language) は、BCG グラフの探索アルゴリズムをプログラミングするための高水準関数型言語です。XTL は、状態、遷移、ラベル、後続関数と先行関数などを処理するためのプリミティブを提供します。たとえば、状態セットの再帰関数を定義できます。これにより、XTL で通常の時相論理 (HML、[ ^7] CTL、^[8] ACTL、^[9]など) の固定小数点アルゴリズムの評価と診断生成を指定できます。

明示的モデル (BCG グラフなど) と暗黙的モデル (オンザフライで探索) 間の接続は、次のような OPEN/CAESAR 準拠のコンパイラによって保証されます。

• • CAESAR.OPEN、LOTOS記述として表現されたモデル用
  • BCG.OPEN（BCGグラフとして表現されるモデル用）
  • EXP.OPEN、通信オートマトンとして表現されたモデルの場合
  • FSP.OPEN、FSP記述として表現されたモデル用
  • LNT.OPEN、LNT記述として表現されたモデルの場合
  • SEQ.OPEN、実行トレースのセットとして表現されるモデルの場合

CADP ツールボックスには、Verimag 研究所 (グルノーブル) と INRIA レンヌの Vertecs プロジェクト チームによって開発された ALDEBARAN や TGV (検証に基づくテスト生成) などの追加ツールも含まれています。

CADPツールはよく統合されており、EUCALYPTUSグラフィカルインターフェースまたはSVL ^[10]スクリプト言語のいずれかを使用して簡単にアクセスできます。EUCALYPTUSとSVLはどちらも、必要に応じてファイル形式の変換を自動的に実行し、ツールの呼び出し時に適切なコマンドラインオプションを提供することで、ユーザーにCADPツールへの簡単で均一なアクセスを提供します。

• 2002年、CADPのEVALUATORモデルチェッカーを設計・開発したRadu Mateescuは、ローヌ＝アルプ・フューチャー財団が主催する年次シンポジウムの第10回で情報技術賞を受賞した。^[11]

• 2011年、CADPのソフトウェア設計者兼開発者であるヒューバート・ガラベルがゲイ＝リュサック・フンボルト賞を受賞した。^[12]

• 2019年、フレデリック・ラングとフランコ・マッツァンティは、CADPを使用して、さまざまな通信状態マシンのセットで360の計算ツリー論理（CTL）と線形時相論理（LTL）の式を正しく評価し、RERSチャレンジの並列問題ですべての金メダルを獲得しました。^{[13] [14]}

• 2020年、フレデリック・ラング、フランコ・マッツァンティ、ウェンデリン・セルウェは、RERS'2020チャレンジで「Parallel CTL」問題の88%を正しく解き、90式のうち11式に対してのみ「わからない」と答え、3つの金メダルを獲得しました。^{[15] [16] [17]}

• 2021 年、Hubert Garavel 氏、Frédéric Lang 氏、Radu Mateescu 氏、Wendelin Serwe 氏は、CADP ツールボックスの開発につながった科学的研究により、Inria – Académie des Sciences – Dassault Systèmes のイノベーション賞を共同で受賞しました。^[18]

• 2023年、Hubert Garavel、Frédéric Lang、Radu Mateescu、Wendelin Serweは、CADPツールボックスに対して、ソフトウェア科学のヨーロッパの主要なフォーラムであるETAPSから初のTest-of-Time Tool Awardを共同で受賞しました。 ^[19]

• SYNTAXコンパイラ ジェネレータ (多くのCADPコンパイラとトランスレータの構築に使用)

• 翻訳：
• 翻訳：
• http://convecs.inria.fr/