摘要
采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义。分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法。时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证。最后,结合具体应用给出了应用示例。
Formal specification and verification on complex real-time component system＇s interaction behavior have great significance of improving component systems＇ trustworthy properties such as correctness and reliability.The advantages and disadvantages of using process algebra and automata to model components interaction behavior were analyzed,and timed component interaction automata（TCIA） based modeling methods were presented based on the analysis.The related definition,composition and verification algorithm of TCIA were given.Models based on TCIA can clearly specify components＇ interaction behavior,architecture and real-time information in detail and are convenient to verify.Finally,an application example was introduced.
出处
《计算机科学》
CSCD
北大核心
2010年第9期151-156,共6页
Computer Science
基金
国家自然科学基金项目(90718017
60473057)
博士学科点专项科研基金项目(20070006055)资助
关键词
构件
交互行为
形式化描述
自动机
Component
Interaction behavior
Formal specification
Automata
