构件行为协议实时性扩展及相容性验证

对复杂实时构件系统行为进行形式化描述和相容性验证,可以有效提高系统的正确性、可靠性。分析了学术界和工业界的主流构件模型及常见时间行为的形式化描述方法,对构件行为协议BP(Behavior Protocol)进行了扩展,提出了时间行为协议TBP(Ti med Behavior Protocol),分析了构件组合中常见的相容性错误类型,给出了基于时间行为协议的构件组合相容性验证算法。TBP应用简洁、方便、易于验证。结合具体例子给出了应用示例。

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

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