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

Specification and Compatibility Verification of Timing Behavior in Components

作　　者：张振领[1] 贾仰理[1] 周恩光[2] 李舟军[2] 

机构地区：[1]聊城大学计算机学院,聊城252059 [2]北京航空航天大学计算机学院,北京100191

出　　处：《计算机科学》2012年第10期143-147,共5页Computer Science

基　　金：国家自然科学基金项目(90718017);山东省自然科学基金项目(ZR2011FL023);山东省软科学项目(2010RKE16007);山东省高校智能信息处理与网络安全重点实验室项目资助

摘　　要：利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。It can efficiently improve the system＇s correctness and reliability for specification and verifying of timing behavior in complex real-time components.This paper presented the timed behavior protocol based formal modeling me-thods of timing behavior and the verification method for component-based systems.The architecture of the specification and verification tool named TCBV was given.An application example was introduced and the experimental results show that the timed behavior protocol based specification and verification methods can accurately model and conveniently verifyerrors of timing behavior in complex real-time component systems.Finally,TCBV and other related tools were compared and the differences between them were analyzed.

关 键 词：实时构件系统 时序行为 形式化方法 建模 相容性验证工具 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]