基于自动机的构件实时交互行为的形式化模型

计算机科学 ›› 2010, Vol. 37 ›› Issue (9): 151-156.

基于自动机的构件实时交互行为的形式化模型

贾仰理,张振领,李舟军

(聊城大学计算机学院聊城252059);(北京航空航天大学计算机学院北京100191)

出版日期:2018-12-01 发布日期:2018-12-01
基金资助:
本文受国家自然科学基金项目(90718017,60473057),博上学科点专项科研基金项目(20070006055)资助。

Formal Model of Component Real-time Interaction Behavior Based on Automata Theory

JIA Yang-li,ZHANG Zhen-ling,LI Zhou-jun

Online:2018-12-01 Published:2018-12-01

摘要/Abstract

摘要： 采用形式化方法对复杂实时构件系统交互行为进行描述和验证，对于提高系统的正确性、可靠性等可信性质具有重要意义。分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点，在此基础上提出了基于时间构件交互自动机的建模方法，给出了时间构件交互自动机的相关定义、组合和验证算法。时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念，既能够描述构件交互情况，又能够清楚地表示出构件系统的体系结构信息和实时信息，便于对系统进行描述和验证。最后，结合具体应用给出了应用示例。

关键词: 构件，交互行为，形式化描述，自动机

Abstract: 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 I}CIA were given. Models based on I}CIA can clearly specify components' interaction behavior, architecture and real-time information in detail and arc convenient to verify.Finally, an application example was introduced.

Key words: Component, Interaction behavior, Formal specification, Automata

贾仰理,张振领,李舟军. 基于自动机的构件实时交互行为的形式化模型[J]. 计算机科学, 2010, 37(9): 151-156. https://doi.org/

JIA Yang-li,ZHANG Zhen-ling,LI Zhou-jun. Formal Model of Component Real-time Interaction Behavior Based on Automata Theory[J]. Computer Science, 2010, 37(9): 151-156. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed