构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.

Research of Modeling and Verification of Component-based Real-time System

Using component based software design method in complex real-time system development has become a hot research topic.Verify whether the real-time software meets the given time requirement and reduce the complexity of the verification process is one of the main challenges in real-time computing research area.This paper proposes timed interface model and using it for formal modeling the interactions between component interfaces.Based on interface automata theory the timed interface automata is proposed and used to describe the action and composition of components under the interaction of timed interface.To cope with state space exploration problem,the product of timed interface automata models of components is reduced by eliminating incorrect states before verifying related properties.A simple example through this paper is studied in detail to illustrate how to apply the proposed approach.