在面向服务的架构中,如何根据系统资源环境的变化以及构件的功能和实时性等QoS属性动态组合已有的功能构件以满足应用需求,成为当前此领域的一个研究热点。由于采用非形式化(自然语言)和半形式化(图表)方法描述实时服务系统均存在不精确、歧义的及不易验证等缺陷,而形式化方法能较好地克服上述不足,可充分表述系统的各种特性,并为系统的验证、实现等提供良好的基础。本文提出了一种结合OCL与HTA的实时服务构件(Real-Time ServiceComponent)形式化描述方法:用OCL描述构件的静态语义特征,用HTA描述构件的动态抽象行为;前者为后者的正确性提供属性约束,后者提供前者所描述需求的具体实现,两者语义互补。主要内容及其贡献包括:(1)提出一种基于特征的构件语义描述模型,首先分别给出特征、特征空间和构件特征空间表示模型的定义。接着将构件特征间的各种关联和依赖关系分成自身约束、父子关系约束、显性约束和隐性约束四类,并采用对象约束语言对这些关系进行形式化描述,从而为模型提供了精确的语义支持。面向电子商务的构件特征子树的实例研究及其模型验证和实验结果证明了该模型的正确性与有效性。(2)采用HTA形式化描述实时服务构件的动态抽象行为。给出实时服务构件的HTA模型,系统阐述构件间的各种组装方式及其形式模型,分析构件组装的语法可组合性和语义可组合性问题。采用HTA可层次地构造实时系统集成框架,较高层次的实时服务构件的行为可通过由较低层次的构件组成的HTA来定义。该模型的显著特点是简单容易理解,能在一个统一的框架中表示构件的组装、行为和分析系统性能,适用于不同粒度的实时服务构件集成,有效降低了实时服务系统的复杂度,从而使模型验证工具能够处理更为复杂的服务系统。(3)提出一种基于MLTS的实时服务构件HTA模型组装验证算法。给出(层次)自动机到标号迁移系统的转换过程,在标号迁移系统的扩展模型—多集标号迁移系统基础上,给出其组装算法,利用共享动作是否转换为内部动作来判定模型的组装兼容性。该算法能够有效降低状态空间爆炸给模型实例检测带来的难度,同时利用了MLTS能够描述系统同步、异步动作的特点,不仅可以跟踪构件组装前后的状态变化,而且能够刻画构件的接口行为动作变化,因此,它在基于HTA的实时服务构件模型组装兼容性验证方面具有较强的表达能力。(4)描述一个较简单但又具有典型实时服务系统特征的小额支付视频点播实例应用系统。首先采用自顶向下的方法构建系统,接着采用本文的描述方法对系统级的构件及其组装进行建模、分析和验证,并简单分析了系统的时间属性。