分布式过程的构建与分析

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中的大多数验证算法都是基于标记的过渡系统模型，它由一组状态、一个初始状态和一个过渡状态组成。