tcbv:一种构件时序行为建模与相容性验证工具

利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全彼关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法，给出了时间行为协议建模与相容性验证工具tci3v的系统架构与功能模块。tci3v应用方便，能够实现实时构件时序行为模型的图形化表示，并可对复杂交互行为的相容性进行自动验证。结合应用实例，介绍了如何利用"i'c13v对复杂实时构件系统的时序行为进行建模和验证。最后，将tcbv与其它相关工具进行了比较。