基于时间化UML的安全通信模型检测

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

Safety communication model checking based on timed UML

The model checking method based on timed UML（Unified Modeling Language） is proposed in order to verify the correctness of safety critical system communication model more effectively.Firstly,the safety threats and corresponding defending methods in safe critical system communication environment are modeled by using timed UML.The concurrent state machine diagram of timed UML is also used to model the behaviors of the sender,the channel and the receiver.Secondly,the UML model of the safety communication system is transformed into the timed automata format,which is an identifiable format of timed model checker tools.Finally,the timed automata format model of safety communication system is checked by using timed model checking.The checked properties consist of the model safety properties,the state reach ability properties and the non-deadlock properties.The model checking results not only verify the correctness of this UML model but also prove the validity of the threats defending methods in safety critical system communication.