用形式化语言描述通信与并发，非常经典，用逻辑的思维分析计算机系统中的通信并发问题

基于NuSMV语言描述三层电梯的行为，并对相关性质进行模型检测。是一个模型检测应用的简单例子。

动态故障树是系统安全性分析的常用工具，本资源是动态故障树定性分析的代码实现。