论文部分内容阅读
为了有效验证安全关键系统的通信模型,提出基于时间化UML(unified modeling language,统一建模语言)的模型检测方法。首先采用时间化UML对安全关键通信中的安全威胁和对应的防御手段进行建模,模型中使用并发状态机分别描述发送端、信道和接收端的行为;然后将UML模型转换为时间化自动机形式,作为模型检测工具可识别的输入语言;最后利用模型检测工具对安全关键通信模型的安全性、状态可达性和无死锁性质进行检测。安全关键通信的模型检测结果验证了该模型的正确性,证明了安全通信防御手段的有效性。