Model Checking of Safety Critical Communication Protocol

摘要：

According to the applicability of defenses against the threads in safety critical communication protocol, the interaction process between safety transmission components and the implication of threads defending methods is modeled. The model for safety critical commutation protocol is a network of timed automata, including the automata for sender and receiver and for channel with randomly generated transmission threads. For this model, all the automata progress synchronously and the model checking of safety and liveness properties is performed with UPPAAL model-checker.

关键词： Model checking safety critical communication timed automata communication protocol

作者: Zhang Yi Wei Xueye He Chunming Shi Zengshu

作者单位: School of electronic and information engineering,Beijing Jiaotong University,Beijing 100044 China Ho School of electronic and information engineering,Beijing Jiaotong University,Beijing 100044 China

会议类型: 国际会议

会议名称: The Third International Symposium on Test Automation & Instrumentation(第三届国际自动化测试与仪器仪表学术会议 2010 ISTAI)

会议地点: 厦门

会议语种:英文

页码: 1414-1418

在线出版日期: 2010-05-22（万方平台首次上网日期，不代表论文的发表时间）