一种Web服务合成的事务模型

随着互联网技术的飞速发展,一种新的基于网络的应用程序-Web服务也得到日益广泛的应用,而Web服务合成就是在自治的和异构的现存Web服务基础上被建立起来,本文介绍了一种Web事务处理的模型,可帮助建立高效的Web服务合成,该模型是一种多层的体系结构,我们首先Web事务处理作一般性介绍,其次,对该模型的各个组件分别加以说明,并举例说明其实现(使用扩展的WSDL).     

Composition mechanisms for retrenchment

Retrenchment is a flexible model evolution formalism that arose as a reaction to the limitations imposed by refinement, and for which the proof obligations feature additional predicates for accommodating design data. Composition mechanisms for retrenchment are studied. Vertical, horizontal, dataflow, parallel and fusion compositions are described. Of particular note are the means by which the additional predicates compose. It is argued that all of the compositions introduced are associative, and that they are mutually coherent. Composition of retrenchment with refinement, so important for the smooth interworking of the two techniques, is discussed. Decomposition, allowing finer grained retrenchments to be extracted from a single large grained retrenchment, is also investigated.     

异构软件构件组装模型设计与实现

研究了异构构件组装方法,根据主流构件模型的差异,设计了异构软件构件组装模型,使构件对外呈现一致的构件视图,屏蔽构件的异构性,有效地利用系统资源,最大限度地为应用系统的生成提供支持。     

Vulnerability analysis of networks to detect multiphase attacks using the actor-based language Rebeca

Increasing use of networks and their complexity make the task of security analysis more and more complicated. Accordingly, automatic verification approaches have received more attention recently. In this paper, we investigate applying of an actor-based language based on reactive objects for analyzing a network environment communicating via Transport Protocol Layer (TCP). The formal foundation of the language and available tools for model checking provide us with formal verification support. Having the model of a typical network including client and server, we show how an attacker may combine simple attacks to construct a complex multiphase attack. We use Rebeca language to model the network of hosts and its model checker to find counter-examples as violations of security of the system. Some simple attacks have been modeled in previous works in this area, here we detect these simple attacks in our model and then verify the model to find more complex attacks which may include simpler attacks as their steps. We choose Rebeca because of its powerful yet simple actor-based paradigm in modeling concurrent and distributed systems. As the real network environment is asynchronous and event-based, Rebeca can be utilized to specify and verify the asynchronous systems, including network protocols.     

步进索引模型下的语义及其形式化

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.     

Use Case的分析设计和实现

本文介绍了分析,设计和实现ｕｓｅ ｃａｓｅ的过程,重点阐述ｕｓｅ ｃａｓｅ的描述,细化和实现的有关细节 。     

基于抽象和组合方法的网络协议验证

由于模型检测存在状态爆炸问题,多主体的网络协议组合模型检测往往难以进行。为了缓解该问题,分析了通信主体数量增加对状态数量的影响,提出了组合式的抽象验证方法。首先根据所需验证的LTL性质,建立各个通信主体的Kripke结构,再对该Kripke结构进行抽象;然后组合抽象模型;最后运用Spin对组合抽象模型进行检验。为验证该方法的有效性,对NSPK协议进行了检测,结果表明,该方法所需的状态空间向量长度、搜索深度、存贮和遍历的状态数都有明显减少,有利于缓解状态爆炸问题。     

The living in a lattice rule language

This paper presents a rule-based query language for an object-oriented database model. The database model supports complex objects, object identity, classes and types, and a class/type hierarchy. The instances are described by ‘object relations’ which are functions from a set of objects to value sets and other object sets. The rule language is based on object-terms which provide access to objects via the class hierarchy. Rules are divided into two classes: object-preserving rules manipulating existing objects (yielding a new ‘view’ on objects available in the object base) and object-generating rules creating new objects with properties derived from existing objects. The derived object sets are included in a class lattice. We give conditions for whether the instances of the ‘rules’ heads are ‘consistent’, i.e. represent object relations where the properties of the derived objects are functionally determined by the objects.     

多媒体让作文教学展开奋飞的翅膀

在作文效率不高的困扰之下,多媒体的应用为作文教学插上了奋飞的翅膀。笔者把多媒体应用下的作文教学分为三重境界:第一境界:昨夜西风凋碧树,独上高楼,望尽天涯路。利用多媒体把真实的生活场景摄制、提炼,再现于学生眼前,让学生获得感性认识。第二境界:衣带渐宽终不悔,为伊消得人憔悴。利用多媒体创设真切、动人的情景,调动学生各种感知器官,令其有感可发,有情欲抒,产生强烈的写作欲望。第三境界:众里寻她千百度,蓦然回首,那人却在灯火阑珊处。利用多媒体,精心评改作文,为学生提供鲜明的形象和素材,作具体性的指导。     

Godel语言延迟声明语句的语义及其实现方法

Gdel语言因语言成份复杂而缺乏严格的语义基础和成熟的编译器,因此推出后它一直发展缓慢。对此采用进化代数描述了其主要语言成分延迟声明语句的过程性语义,然后介绍了依据该语义的具体实现方法并给出运行流程图和C语言描述。最后通过一个例子来具体说明延迟计算在基于扩展Warren机的编译系统中的执行情况。实验结果表明了其可行性。     

一种词义与词的混合语言模型及其应用

本文提出了一种基于词和词义混合的统计语言模型,研究了这个模型在词义标注和汉语普通话语音识别中的性能,并且与传统的词义模型和基于词的语言模型进行了对比。这个模型比传统词义模型更准确地描述了词义和词的关系,在词义标注中具有较小的混淆度;在汉语普通话连续音识别中,这个词义模型的性能优于基于词的三元文法模型,并且需要较小的存储空间。     

Haskell语言的高阶特性及其应用

Haskell语言的高阶特性使笔者在开发软件时受益匪浅,但很遗憾,目前国内同行应用这一语言的人非常少。本文介绍Haskell语言的高阶特性,并通过几个与树相关的例子,阐述如何利用Haskell语言的高阶特性来编写功能强大但却简短漂亮的程序。     

Gamma的语义研究

在推导程序属性方面,公理语义比操作语义具有更多的优点。本文定义Gamma 的时态语义,它是已有工作的进一步精确化;本文证明这种时态语义与结构化操作语义是一致的。     

A comparative study of two formal semantics of the SIGNAL language

SIGNAL is a part of the synchronous languages family, which are broadly used in the design of safety-critical real-time systems such as avionics, space systems, and nuclear power plants. There exist several semantics for SIGNAL, such as denotational semantics based on traces (called trace semantics), denotational semantics based on tags (called tagged model semantics), operational semantics presented by structural style through an inductive definition of the set of possible transitions, operational semantics defined by synchronous transition systems (STS), etc. However, there is little research about the equivalence between these semantics. In this work, we would like to prove the equivalence between the trace semantics and the tagged model semantics, to get a determined and precise semantics of the SIGNAL language. These two semantics have several different definitions respectively, we select appropriate ones and mechanize them in the Coq platform, the Coq expressions of the abstract syntax of SIGNAL and the two semantics domains, i.e., the trace model and the tagged model, are also given. The distance between these two semantics discourages a direct proof of equivalence. Instead, we transformthem to an intermediate model, which mixes the features of both the trace semantics and the tagged model semantics. Finally, we get a determined and precise semantics of SIGNAL.     

基于二维QoS模型的Web服务组合

在实际应用中,单个Web服务通常无法满足复杂应用的需求,如何组合已有的服务,从而提供更强大更完整的商业功能已成为此领域的研究热点。然而现行的SOA架构中,Web服务组合方法中很少考虑Web服务质量（QoS）问题,或者对Qos考虑得不够全面,这样,组合出的服务不能确保能够满足用户的QoS需求。针对这一问题,提出了Web服务的二维QoS模型,并使用了改进的UDDI规范,在此基础上给出了基于QoS的Web服务组合的有色Petri网组合策略。在满足用户组合服务的功能需求的同时,也满足了用户对服务质量QoS的需求,实现了需求服务的优化。     

Algebraic Composition of Function Tables

In general, a program is composed of smaller program segments using composition, conditional constructs or loop constructs. We present a theory which enables us to algebraically define and compute the composition of conditional expressions. The conditional expressions are represented using tabular notation. The formal definition of the composition allows us to compute the close form representation of the composition of tabular expressions. The presented approach is based on a many sorted algebra containing information preserving composition. This formal definition of composition is then “lifted” to an extended algebra containing tabular expressions. The presented theory provides very compact algorithms and proofs. Received July 1998 / Accepted in revised form January 2000     

基于移动Agent的服务组合的建模

采用形式化描述Web服务组合,从很大程度上推动了Web服务组合技术的实际应用。但现有的Web服务组合形式化建模方法在利用形式化工具时,均未很好地解决建模的层次性问题。为解决上述问题,提出了将Web服务组合问题映射为一个基于移动Agent的层次化服务组合模型,系统模型分为系统服务层和Agent层。模型设计充分体现了移动Agent的移动性、自主性以及系统层(移动Agent运行环境)的控制性。最后给出实例说明该方法。     

教育评估系统模型的设计与实现

评估工作计算机化,可以减少人为的错误与客观因素干扰,增强评估的稳定、透明与公正性.本文论述了教育评估计算机模型的设计和实现,包括系统结构以及角色安全模型、量化模型、智能约束模型等建模技术.