基于高阶π演算的构件演化行为研究

用形式化的方法分析软件演化过程中构件的行为已成为目前构件开发中的研究热点。为了满足构件演化过程中行为建模形式化的需要,建立了一种基于高阶π演算的构件演化行为分析方法。对构件演化行为进行分类,将顺序图表示的演化请求转换成高阶π演算进程表达式,通过高阶π演算的语法语义和等价理论等数学基础对演化行为进行推演,并检测演化中是否存在死锁问题。最后通过实例对该方法进行分析说明,从而验证了该方法的可行性和有效性。     

基于高阶π演算的构件演化模型研究*

为满足构件演化形式化分析的需要,确保演化正确性,提出了一种基于高阶π演算的构件演化模型。在定义演化构件的基础上,将演化过程中的行为描述为原子行为、结构行为和操作行为,建立行为与高阶π演算间的转换规则、演化行为推演规则,根据演化过程中行为之间的关系,建立演化冲突检测机制,定义互斥冲突、重复冲突、条件冲突和包含冲突等四类冲突,在分析冲突条件的基础上,设计了演化冲突检测算法,实现了构件演化的形式化分析。通过实例验证了模型的可行性。     

基于逻辑推理的构件组装策略及其算法

针对构件组装体系框架,提出一种适用于无状态构件的组装策略,用于满足用户的构件检索请求．该策略通过进程代数理论形式化描述构件行为,提高匹配度,并提出了2 种基于逻辑推理的检索算法SABLR（searchingalgorithm based on logical reasoning）和ASABLR（advanced searching algorithm based on logical reasoning）加以支持．检索算法均应用正向推理的思想,判别构件仓库中是否含有用户请求构件信息．算法可以判别2 种状况：一是库中直接含有请求构件信息,二是库中部分构件可经组装后满足用户请求．克服了普通构件检索算法无法判别第2 种状况的缺点．最后,通过实例分析和算法ASABLR 的实现,证明该策略的有效性和可行性．     

基于Pi演算的构件行为兼容性研究*

构件行为的兼容性分析是研究构件动态交互过程中的重要问题,其研究结果可应用于构件替换、迁移、动态自适应演化等研究。为了保证构件在替换或组合之后系统仍能正常稳定运行,利用Pi演算对构件行为进行建模,并对多个构件行为间的兼容性进行验证,提出了绝对兼容、相对兼容等理论,并运用兼容度来判定构件行为兼容性强弱,且通过实例进行分析说明。     

基于行为描述的软件构件组合兼容性检查

定义构件的基调视图和行为视图,给出将构件行为转化为π演算进程表达的建模方法,并设计实现构件行为的π演算描述自动转换的算法。结合一个电子商务的实例,借助π演算的操作语义和形式化推理技术实现对软件构件组合时的兼容性进行检查。     

网络服务行为的进程代数验证方法研究及其应用

通过形式化建模分析了系统特点,确认系统行为,从而尽可能避免系统的冲突等情况.文中提出了一种使用进程代数描述网络服务组件的行为建模方法,包括强模拟、强互模拟、时效性、触发器、服务环境等网络服务交互行为描述方法,然后给出了P2P节点的节点发现、防火墙穿越等行为的描述,提出了适用于托管的RCMMS网络自管理协议,并使用代数的...     

基于构件重组的分布式业务集成系统设计与实现

针对分布式环境下业务系统的动态集成技术,设计并实现了一种基于构件重组的分布式业务集成系统,基于这种系统集成架构,可以实现分布式业务系统的智能化的构建和动态重组,提高了业务系统构建的灵活性和构建效率,增强了业务系统可重用性、可维护性。     

基于范畴论的构件行为组合研究

针对基于构件开发过程中单个构件功能难于满足用户需求的问题,提出一种利用范畴论对构件行为进行组合的方法,用以实现复杂的业务功能。采用范畴论给出构件的形式语义描述,构件与构件之间的行为交互关系采用图表进行建模。给出一种基于图表推出的构件行为组合方法与推出运算的算法实现。实际应用结果表明,该方法对构件的形式化描述更加精确,构件组合也更加有效快捷。     

构件行为模型的构造研究

提出了基于 UML构件规格说明自动构造构件行为模型的方法 ,并用一个实例对该方法进行了说明。该方法构造的构件行为模型包含状态与状态之间的转换 ,接口操作作为状态转换弧上的输入 ,能够很好地体现接口的操作调用序列 ,因而可以作为构件测试的测试模型 ,对于构件的开发者和使用者进行构件的黑盒测试以及第三方构件的评估很有价值。     

CORBA构件组装技术研究与应用

本文在对CORBA构件模型以及构件组装技术进行研究的基础上,分析了基于CORBA构件模型的构件组装机制及构件组装的描述方法。在研究的基础上设计出一个具体的构件组装工具,并用此组装工具组装我们的构件,实现了应用系统-水位报警系统。     

一个可扩展的OO构件模型的设计

基于构件的软件开发模式是大规模软件复用的一条切实可行的途径。近二十年来面向对象技术的迅速发展为这种开发模式提供了必要的技术支持。从软件设计范型的角度出发可以将构件分为OO构件和非OO构件两类,本文针对OO构件提出了一个简明的OO构件模型和OO构件描述语言,能够描述OO方法学中一些最常用的软件形态,为OO构件的制作、检索和组装提供一种易于实现的基础支持。     

一种构件化动态软件系统组态模型*

在讨论软件构件技术复用现状的基础上,借鉴工业控制领域的组态概念,提出了一种构件化动态软件系统组态模型。其基本思想是：在一定的软件体系结构基础上,用系统的宏观逻辑组态描述联结实现系统具体功能的软件构件,定制组装成完整的应用系统。构件化大大提高软件开发的速度和效率,逻辑和实现的分离明显改善软件系统的灵活性和逻辑可扩充性,系统逻辑组态描述能始终保持软件系统应用和需求的一致性。     

面向对象的可信构件网的组装研究

以当前可信软件研究中的一个热点问题——基于构件的可信软件构造及其关键理论和技术为主要内容开展研究工作。在前期的工作中,根据面向对象的思想对Petri网进行扩展,提出了基于面向对象思想的可信构件网,从而 对构建的基于构件的可信软件模型中的可执行的构件集进行描述。 在描述的可信构件网模型框架中,将讨论两个构件基于连接件的并行组装、选择组装、顺序组装、循环组装。通过连接件的连接作用,根据一定的组织关系协调构件之间的关系,最终将组合的构件形成一个有机的整体。     

基于CCM的应用服务器及关键技术研究

CCM是CORBA3．0规范中提出的服务器端构件标准。本文在深入研究CCM的基础上,结合CCM和应用服务器技术的优点,提出了一个易于管理、可重用、可伸缩、健壮的基于CCM的应用服务器中间件集成框架,并对其关键技术进行了深入探讨。     

Failure-free coordinators synthesis for component-based architectures

One of the main problems in component assembly is how to establish properties on the assembly code by only assuming a limited knowledge of the single component properties. Our answer to this problem is an architectural approach in which the software architecture imposed on the assembly prevents black-box integration anomalies. The basic idea is to build applications by assuming a “coordinator-based” architectural style. We, then, operate on the coordinating part of the system architecture to obtain an equivalent version of the system which is failure-free. A failure-free system is a deadlock-free one and it does not violate any specified coordination policy. A coordination policy models those interactions of components that are actually needed for the overall purpose of the system. We illustrate our approach by means of an explanatory example and validate it on an industrial case study that concerns the development of systems for safeguarding, fruiting, and supporting the Cultural Heritage.     

Using typed lambda calculus to implement formal systems on a machine

Much research has been devoted in building computer systems for checking proofs or for developing interactively correct proofs in specific logical systems. However, implementing a proof environment for a specific logical system is both complex and time-consuming, this-together with the proliferation of logics-suggests that a uniform and reliable alternative is desirable. One such alternative is the Edinburgh Logical Framework (LF), developed in the late eighties at the LFCS (Laboratory for Foundations of Computer Science). The LF is a logic-independent tool which, given a specification for a logical system, synthesizes a proof editor and checker for that system. Its specification language is based on a general theory of logics, which enables one to capture uniformities and idiosyncrasies of a large class of logics without sacrificing generality for tractability. Peculiarities (such as side conditions on rule application, variable occurrence or formula formation) are expressed at the level of the specification. In this paper we are going to provide a broad illustration of its applicability and discuss to what extent it is successful. The analysis (of the formal presentation) of a system carried out through encoding often illuminates the system itself. This paper will also deal with this phenomenon.     

一种面向Web复合服务的运行时监控方法

随着计算机技术的发展,软件面临着日益严峻的可信性要求,运行时监控技术作为保证软件可信性的一个重要方法,已受到人们的普遍关注。分析总结传统软件运行时监控技术的基本问题和方法,给出运行时监控的基本视图。针对Web复合服务面临的特殊运行环境及监控需求,提出一种监控框架。该框架以事件计算建模行为规约,在无法对构件服务进行插装的情况下实现对复合服务的有效监控。     

Formalizing the specification and execution of workflows using the event calculus

The event calculus is a logic programming formalism for representing events and their effects especially in database applications. This paper proposes the event calculus as a logic-based methodology for the specification and execution of workflows. It is shown that the control flow graph of a workflow specification can be expressed as a set of logical formulas and the event calculus can be used to specify the role of a workflow manager through a set of rules for the execution dependencies of activities. The proposed framework for a workflow manager maintains a history of events to control the execution of activities. The events are instructions to the workflow manager to coordinate the execution of activities. Based on the already occurred events, the workflow manager triggers new events to schedule new activities in accordance with the control flow graph of the workflow. The net effect is an alternative approach for defining a workflow engine whose operational semantics is naturally integrated with the operational semantics of a deductive database. Within this framework it is possible to model sequential and concurrent activities with or without synchronization. It is also possible to model agent assignment and execution of concurrent workflow instances. The paper, thus, contributes a logical perspective to the task of developing formalization for the workflow management systems.