基于协议的实时构件行为一致性验证

摘要

对复杂实时构件系统行为进行形式化描述和一致性验证,可以提高实时构件的可复用性和系统的正确性、可靠性.分析了时间行为协议TBP(Timed Behavior Protocol)及其它学术界和工业界常用的时序行为形式化描述方法,对实时构件替换理论进行了讨论,给出了基于时间行为协议的构件一致性验证算法并对其进行了分析.%The formal specification and consistency verification of complex real-time component systems' behavior can efficiently improve the systems' reusability, correctness and reliability. This paper analyzed the timed behavior protocol and the other mainstream formal specification methods of real-time behavior used in academia and industry. Based on the analysis we gave the substitution theory and the consistency verification algorithm based on timed behavior protocol, which can support complex real-time component based systems' development