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

CADP [1] (分散プロセスの構築と分析) は、通信プロトコルと分散システムの設計のためのツールボックスです。CADPは、INRIAローヌ＝アルプのCONVECSチーム（旧VASYチーム）によって開発され、様々な補完ツールと連携しています。CADPはメンテナンスされ、定期的に改良され、多くの産業プロジェクトで利用されています。

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

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

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

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

歴史

CADPの開発は1986年に始まり、最初の2つのツールであるCAESARとALDEBARANの開発が着手されました。1989年には、CAESAR/ALDEBARAN Distribution Package（CAESAR/ALDEBARAN配布パッケージ）の略称であるCADPが誕生しました。その後、ツールの提供を可能にするプログラミングインターフェースなど、いくつかのツールが追加され、CADPの略称はCAESAR/ALDEBARAN Development Package（CAESAR/ALDEBARAN開発パッケージ）となりました。現在、CADPには50以上のツールが含まれています。略称はそのままに、ツールボックスの名称は、その目的をより明確に表すように「分散プロセスの構築と分析」に変更されました 。

メジャーリリース

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

コードネーム 日付
「A」…「Z」 1990年1月 – 1996年12月
トゥエンテ 1997年6月
リエージュ 1999年1月
オタワ 2001年7月
エディンバラ 2006年12月
チューリッヒ 2013年12月
アムステルダム 2014年12月
ストーニーブルック 2015年12月
オックスフォード 2016年12月
ソフィア・アンティポリス 2017年12月
ウプサラ 2018年12月
ピサ 2019年12月
オールボー 2020年12月
ザールブリュッケン 2021年12月
キスタ 2022年12月
アーヘン 2023年12月
アイントホーフェン 2024年12月

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

CADPの機能

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には、強力な時相論理である様相ミュー計算のためのモデル検査ツールが含まれています。様相ミュー計算は、型付き変数と式で拡張され、モデルに含まれるデータに対する述語を表現できます。この拡張により、標準的なミュー計算では表現できないプロパティ（例えば、任意の実行パスに沿って特定の変数の値が常に増加するという事実など）が表現されます。

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

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

言語とコンパイル技術

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

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

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

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

ライセンスとインストール

CADPは大学や公的研究機関に無料で配布されています。産業界のユーザーは、非商用利用のための評価ライセンスを一定期間取得できます。評価期間終了後は、正式ライセンスが必要となります。CADPのコピーをご希望の場合は、登録フォームにご記入ください。[3] ライセンス契約に署名後、CADPのダウンロードとインストール方法の詳細をお知らせいたします。

ツールの概要

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

  • CAESAR.ADT [4]は、 LOTOSの抽象データ型を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（Binary Coded Graphs）は、非常に大きなグラフをディスク上に（効率的な圧縮技術を用いて）保存するためのファイル形式であると同時に、分散処理のためのグラフの分割など、この形式を扱うためのソフトウェア環境でもあります。多くのツールが入出力にこの形式を利用しているCADPにおいても、BCGは重要な役割を果たしています。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]
  • 2019年、フレデリック・ラングとフランコ・マッザンティは、CADPを使用して、さまざまな通信状態マシンのセットで360の計算木論理（CTL）と線形時相論理（LTL）の式を正しく評価することに成功し、RERSチャレンジの並列問題ですべての金メダルを獲得しました。[13] [14]
  • 2020年、フレデリック・ラング、フランコ・マッツァンティ、ウェンデリン・セルウェは、RERS'2020チャレンジで「並列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]

参照

参考文献

  1. ^ Garavel H, Lang F, Mateescu R, Serwe W: CADP 2011: 分散プロセスの構築と分析のためのツールボックス International Journal on Software Tools for Technology Transfer (STTT), 15(2):89-107, 2013年4月
  2. ^ ISO 8807、時間順序仕様の言語
  3. ^ CADPオンライン申請フォーム. Cadp.inria.fr (2011年8月30日). 2014年6月16日閲覧。
  4. ^ H. Garavel. LOTOS抽象データ型のコンパイル、第2回国際形式記述技術会議FORTE'89（カナダ、バンクーバー）の議事録、ST Vuong（編集者）、北ホランド、1989年12月、p.147-162。
  5. ^ H. Garavel, J. Sifakis. LOTOS仕様のコンパイルと検証,第10回プロトコル仕様、テスト、検証に関する国際シンポジウム（カナダ、オタワ）の議事録, L. Logrippo, RL Probert, H. Ural（編集者）, North-Holland, IFIP, 1990年6月, p. 379–394.
  6. ^ H. Garavel. OPEN/CÆSAR: 検証、シミュレーション、テストのためのオープンソフトウェアアーキテクチャ、システムの構築と分析のためのツールとアルゴリズムに関する第1回国際会議TACAS'98（ポルトガル、リスボン）の議事録、ベルリン、B. Steffen（編集者）、Lecture Notes in Computer Science、完全版はInria Research Report RR-3352として入手可能、Springer Verlag、1998年3月、第1384巻、68～84ページ。
  7. ^ M. Hennessy, R. Milner.非決定性と並行性に関する代数法則, Journal of the ACM , 1985年, vol. 32, p. 137–161.
  8. ^ EM Clarke, EA Emerson, AP Sistla.時相論理仕様を用いた有限状態並行システムの自動検証, ACM Transactions on Programming Languages and Systems , 1986年4月, 第8巻第2号, 244–263ページ.
  9. ^ R. De Nicola, FW Vaandrager.遷移システムにおけるアクションベースロジックと状態ベースロジックの比較, Lecture Notes in Computer Science , Springer Verlag, 1990, vol. 469, p. 407–419.
  10. ^ H. Garavel、F. Lang、 「SVL: 構成検証用のスクリプト言語」、Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea)、M. Kim、B. Chin、S. Kang、D. Lee (編集者)、完全版は Inria Research Report RR-4223 として入手可能、Kluwer Academic Publishers、IFIP、2001 年 8 月、p. 377–392。
  11. ^ “ラドゥ・マテスクがローヌ・アルプ・フトゥール財団から与えられたIT賞を受賞”.
  12. ^ Isabelle Bellin (2011年4月16日). 「Hubert Garavelがゲイ＝リュサック・フンボルト研究賞を受賞」. 2016年7月10日時点のオリジナルよりアーカイブ。
  13. ^ 「RERSチャレンジ2019の結果」。
  14. ^ 「CADPニュースレター第12号 - 2019年4月10日」。
  15. ^ 「RERSチャレンジ2020の結果」。
  16. ^ 「CNR-Inria チームが RERS 2020 Parallel CTL Challenge で金メダルを獲得」。
  17. ^ 「CADPニュースレター第13号 - 2021年2月22日」。
  18. ^ 「Convecs チームが並列システムのセキュリティを強化」。
  19. ^ 「ETAPS Test-of-Time Tool Award」.
  • http://cadp.inria.fr/
  • http://vasy.inria.fr/
  • http://convecs.inria.fr/
「https://en.wikipedia.org/w/index.php?title=分散プロセスの構築と分析&oldid=1321401205」より取得