分布式過程的構建與分析

CADP（分布式過程的構建與分析）是一個用于設計通信協議和分布式系統的工具箱。CADP得到維護，定期改進，并在許多工業項目中使用。CADP工具箱的目的是通過使用形式化描述技術以及用于仿真、快速應用開發、驗證和測試生成的軟件工具來促進可靠系統的設計。CADP可以應用于任何包含異步并發的系統，也就是說，任何系統的行為都可以被建模為一組由交錯語義支配的并行進程。因此，CADP可用于設計硬件結構、分布式算法、電信協議等。CADP中實現的枚舉式驗證（也稱為顯式狀態驗證）技術，雖然沒有定理證明那么通用，但可以自動、經濟地檢測復雜系統中的設計錯誤。CADP包括支持使用形式化方法中的兩種方法的工具，這兩種方法都是可靠系統設計所需要的。模型為并行程序和相關的驗證問題提供數學表示。模型的例子有自動機、通信自動機網絡、Petri網、二進制決策圖、布爾方程系統等。從理論的角度來看，對模型的研究尋求一般的結果，與任何特定的描述語言無關。在實踐中，模型往往過于初級，不能直接描述復雜的系統（這將是乏味和容易出錯的）。這項任務需要一個更高層次的形式主義，即過程代數或過程微積分，以及將高層次描述轉化為適合驗證算法的模型的編譯器。目前CADP包含50多個工具。在保持相同的縮寫的同時，工具箱的名稱已經改變，以更好地表明其目的：分布式過程的構建和分析。

CADP的發布版本先后以英文字母（從A到Z）命名，然后以積極從事LOTOS語言研究的學術研究小組所在城市的名稱命名，更廣泛地說，以對并發理論作出重大貢獻的城市名稱命名。在主要版本之間，經常會有次要版本，提供對新功能和改進的早期訪問。更多信息請見CADP網站上的變更列表頁面。CADP的特點CADP提供了一系列廣泛的功能，從分步仿真到大規模并行模型檢查。它包括多個輸入形式的編譯器：用ISO語言LOTOS編寫的高級協議描述。該工具箱包含兩個編譯器，將LOTOS描述翻譯成C代碼，用于仿真、驗證和測試。指定為有限狀態機的低層次協議描述。

通信自動機網絡，即。幾個等價檢查工具（最小化和比較雙映射關系），如BCG_MIN和BISIMULATOR。幾個模型檢查器，用于各種時間邏輯和μ微積分，如EVALUATOR和XTL。幾個驗證算法相結合：枚舉式驗證、即時驗證、使用二進制決策圖的符號驗證、組合式最小化、部分命令、分布式模型檢查等。加上其他具有高級功能的工具，如可視化檢查、性能評估等。CADP以模塊化的方式設計，將重點放在中間格式和編程接口上（如BCG和OPEN/CAESAR軟件環境），這使得CADP工具可以與其他工具結合，并適應各種規范語言。

驗證是將一個復雜的系統與一組表征系統預期功能的屬性進行比較。CADP中的大多數驗證算法都是基于標記的過渡系統模型，它由一組狀態、一個初始狀態和一個過渡狀態組成。