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

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