安全通信协议规范分层模型检验方法

为合理控制复杂安全通信协议规范模型状态空间的体积,清晰完备地发现协议规范的死锁、活锁和属性缺陷,提出1种根据协议固有层次逐层建模和检验的方法。使用接口自动机网络(IAN)对目标层的上下层进行深入提取,抽象出协议规范的3层模型。依据由IAN模型至着色Petri网(CPN)模型的转化规则,将建立的IAN模型转换为CPN模型;提出利用模型检验工具CPN Tools检验扩展语言ASK-CTL描述的具有存在一致性和前向强制一致性2类属性的方法。选择列车运行控制系统安全通信协议的安全功能模块规范进行实例研究。结果表明:提出的分层模型检验方法,可将模型状态空间的体积控制在要求的规模以内;安全通信协议的安全功能模块规范不存在死锁和活锁,说明安全功能模块流程设计合理;但存在安全功能模块连接建立过程不成功、高优先级数据无法传输和车地间通信连接断开的情况,因此列车控制系统应用层应具备连接功能失效的响应处理流程,以及故障导向安全的防护功能。