基于组合连接器的动态软件体系结构规范方法

动态体系结构的建模与分析是复杂软件体系结构设计的一个重要问题.本文用组合连接器扩展了体系结构描述语言Wright,并由此提出了一种规范动态体系结构的形式化方法.为了支持动态机制,还提出了动态角色的概念.通过实例说明,该方法能将动态体系结构的两种基本形态的描述统一起来,并能为动态软件体系结构设计提供一种增量式的开发方法.由于该方法基于组合的机制,从而适用于体系结构重用.     

采用函数式语言的BPEL模型形式化验证方法

通信顺序进程(communicating sequential process,CSP)是一种经典的形式化方法,CSP_M是在CSP基础上提出的一种函数式语言。目前Web服务组合中BPEL(business process execution language)模型缺乏可执行的形式化编程语言,通过CSP_M提出了一种基于函数式语言的BPEL模型验证方法。首先给出了基于CSP_M的BPEL模型建模与验证框架;其次给出了CSP_M的进程代数定义;再次详细描述了BPEL语言到CSP以及CSP_M的映射方法;最后以一个在线购物系统为例,讨论了该方法的使用效果。实验表明该方法可以提高BPEL模型的可靠性。     

安全协议的CSP描述技术

基于进程代数的CSP方法是一种重要的形式化协议分析验证方法。本文首先简单介绍了CSP相关理论,并以NSPK协议为例系统概述了安全协议的CSP建模方法。为更好的查明协议的安全缺陷,重点研究如何在CSP的体系结构中对协议的安全属性进行形式化描述。并最终提出秘密性、认证性、不可否认性、匿名性的形式化提炼检测目标,为进一步使用模型检测器进行协议验证奠定了理论和技术基础。     

基于组合连接器的潜在无限动态结构的规范

动态软件体系结构的建模与分析是复杂软件系统设计的一个重要问题。基于体系结构描述语言Wright，提出了一种规范潜在无限动态结构的形式化方法。为了便于使用递归机制，引入了组合连接器和动态角色的概念，从而实现了动态体系结构的逐层展开。实例说明，该方法能为动态体系结构的设计提供一种增量式的开发方式，适用于连接器重用的目的。     

一种安全协议组合分析方法*

提出了一种安全协议组合分析方法,即使用通用认证协议规范语言CAPSL描述安全协议,然后使用连接器,将CAPSL规范转换为其他安全协议分析工具的形式化输入,从而能够利用不同分析工具的优点,来更好地保证安全协议形式化分析的准确性,同时也方便了安全协议分析者。设计了两个CAPSL连接器,并给出一个协议转换实例。     

一种基于认知模型检测的Web服务组合验证方法

近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法,将Web服务组合建模为多主体系统,在分析BPEL语言控制流程基础上,提出BPEL活动的形式化模型,给出活动执行...     

认证协议两种形式化分析方法的比较

串空间模型和CSP方法是当前最著名的分析认证协议的形式化方法.通过一个具体的认证协议例子,比较两种方法的不同特点.     

基于通信序列进程的UML序列图形式化方法

UML2.0序列图是一种描述对象之间动态协作和事件发展时间关系的视图,但是UML序列图缺乏精确的形式化语义,所以不利于对其所描述的系统进行形式化验证。为此,根据UML2.0语义文档及组合碎片包概念,基于通信序列进程(CSP)给出了UML序列图的基本元素和消息迹的形式化定义及生成规则,实现了UML序列图的形式化,为UML序列图在描述系统准确性和有效性方面提供了形式化的检验方法。最后通过ATM实例说明UML序列图这一过程的正确性。     

基于CSP的OWL-S语义分析与建模

为了实现OWL-S过程模型正确性的自动化验证,提出了基于进程代数CSP的OWL-S过程模型的语义建模方法,建立了CSP的形式化语义模型,并利用该模型为OWL-S过程定义了形式化语义。最后以机票预订为例说明了采用CSP模型为OWL-S过程添加形式化语义的完整流程。由于该方法具备良好的数学基础,所以可以基于该方法开发出自动化验证OWL-S过程模型的工具,提高系统的安全性。     

一种混合的安全协议分析方法

在安全协议的形式化分析中,有两种完全不同的观点:模态逻辑和可证安全,两者各有优缺点.目前,将两者进行组合优化,建立统一的调和方法框架对安全协议进行分析是研究的热点和难点.通过对两种观点的研究,按照优势互补的原则将两者相调和,提出了一种新的形式化分析方法,该方法可提供更为完全的安全协议形式化分析.     

软件复合连接件的形式化研究

基于构件的软件开发是软件开发的主流范型。构件通过连接件进行连接和交互。连接件是软件系统设计的一阶实体(First-class Entities),是决定软件系统功能和质量的重要因素。伴随软件系统和构件的规模及复杂程度日益增加,连接件变得愈加复杂和多样。因此,需要运用增量、合成的方法开发和支持复杂的连接件。本文提出一种根据已有连接件合成新连接件的形式化方法。该方法的特点是定义连接件合成的基本方式,即连接件运算符,组合运用连接件运算符合成复杂的连接件。并基于Wright连接件的形式化规约,给出了谊复合连接件形式化规约的生成算法。     

A novel approach to predict shear strength of tilted angle connectors using artificial intelligence techniques

Shear connectors play a prominent role in the design of steel-concrete composite systems. The behavior of shear connectors is generally determined through conducting push-out tests. However, these tests are costly and require plenty of time. As an alternative approach, soft computing (SC) can be used to eliminate the need for conducting push-out tests. This study aims to investigate the application of artificial intelligence (AI) techniques, as sub-branches of SC methods, in the behavior prediction of an innovative type of C-shaped shear connectors, called Tilted Angle Connectors. For this purpose, several push-out tests are conducted on these connectors and the required data for the AI models are collected. Then, an adaptive neuro-fuzzy inference system (ANFIS) is developed to identify the most influencing parameters on the shear strength of the tilted angle connectors. Totally, six different models are created based on the ANFIS results. Finally, AI techniques such as an artificial neural network (ANN), an extreme learning machine (ELM), and another ANFIS are employed to predict the shear strength of the connectors in each of the six models. The results of the paper show that slip is the most influential factor in the shear strength of tilted connectors and after that, the inclination angle is the most effective one. Moreover, it is deducted that considering only four parameters in the predictive models is enough to have a very accurate prediction. It is also demonstrated that ELM needs less time and it can reach slightly better performance indices than those of ANN and ANFIS.

     

Finite strip analysis of curved composite girders with incomplete interaction

This paper presents a finite strip analysis of curved composite girders with incomplete interaction. In the present analysis curved composite girder bridges are modelled by curved strip elements for the concrete slab and steel girder and spring elements for the shear connectors. The shear connectors are assumed as a two-dimensional spring element along the nodal line. The proposed method is applied to the analysis of curved box girders, curved plates and curved composite girder bridges with complete and incomplete interaction. Some analytical results obtained by this method are compared with the test results and theoretical values obtained by other methods, and they are in good agreement. Slip behavior of curved composite box girders is also discussed based on the results by the proposed method.     

一种从Object—Z到CSP规格说明的转化方法

面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。     

Managing dynamic CSPs with preferences

We present a new framework, managing Constraint Satisfaction Problems (CSPs) with preferences in a dynamic environment. Unlike the existing CSP models managing one form of preferences, ours supports four types, namely: unary and binary constraint preferences, composite preferences and conditional preferences. This offers more expressive power in representing a wide variety of dynamic constraint applications under preferences and where the possible changes are known and available a priori. Conditional preferences allow some preference functions to be added dynamically to the problem, during the resolution process, if a given condition on some variables is true. A composite preference is a higher level of preference among the choices of a composite variable. Composite variables are variables whose possible values are CSP variables. In other words, this allows us to represent disjunctive CSP variables. The preferences are viewed as a set of soft constraints using the fuzzy CSP framework. Solving constraint problems with preferences consists in finding a solution satisfying all the constraints while optimizing the global preference value. This is handled by four variants of the branch and bound algorithm, we propose in this paper, and where constraint propagation is used to improve the time efficiency in practice. In order to evaluate and compare the performance of these four strategies, we conducted an experimental study on randomly generated dynamic CSPs with quantitative preferences. The results are reported and discussed in the paper.     

Interactive tool support for CSP || B consistency checking

CSP || B is an integration of two well known formal notations: CSP and B. It provides a method for modelling systems with both complex state (described in B machines) and control flow (described as CSP processes). Consistency checking within this approach verifies that a controller process never calls a B operation outside its precondition. Otherwise the behaviour of the operation cannot be predicted. In previous work, this check was carried out by manually decomposing the model before preprocessing the CSP processes to perform a hand-written weakest precondition proof. In this paper, a framework is described that mechanises consistency checking in a theorem prover and removes the need for preprocessing. This work is based on an existing PVS embedding of the CSP traces model, but it is extended by introducing a notion of state so that the interaction between processes and machines can be analysed. Numerous rules have been defined (and proved) which enable consistency checking and decomposition via PVS proof. These rules also formally justify the relaxation of previous constraints on CSP || B architectures, thereby widening the scope of CSP || B modelling. The PVS embedding and rules presented in this paper are not only applicable to CSP || B specifications, but to other combined approaches which use a non-blocking semantics for the state-based operations. R. Lazic, R. Nagarajan and J. C. P. Woodcock     

基于Petri网的CSP并发系统验证技术研究

通信顺序进程(CSP)和Petri网是两种重要的并发系统建模工具。CSP语言具有高度抽象性,可有效刻画并发进程之间的各种相互作用,但在物理结构的描述与验证分析方面显得不足。Petri 网是一种形式化、图形化的并发系统建模和分析工具,侧重于系统的物理结构描述和性质分析。结合两者优点,首先利用CSP描述待验证的并发系统,然后将其转化为Petri网来分析系统的动态行为特性,最后利用性质分析工具TINA对系统性质进行分析和验证。实验结果表明,传统的CSP进程性质验证工具不能验证CSP进程的安全性,但其转化为Petri网后可有效地分析出导致安全性不能满足的危险因素,从而扩大了CSP描述的并发系统可验证性质的范围。     

Universal RS232C cable

Manufacturers of peripherals are inconsistent in their use of male or female connectors on their equipment. Combined with the increasingly common practice of producing data terminal equipment that in some respects is like data communication equipment (to cut the costs of extra null modem cables), this means that it can be very difficult to make two devices communicate over an RS232C serial link. The paper addresses the problems of incompatible male-female D-type connectors and reversed transmit-receive lines for three-wire communication. These ideas could be expanded for the problems associated with incompatible handshake lines.     

Compositional checking of satisfaction

We present a compositional method for deciding whether a process satisfies an assertion. Assertions are formulas in a modal -calculus, and processes are drawn from a very general process algebra inspired by CCS and CSP. Well-known operators from CCS, CSP, and other process algebras appear as derived operators. The method iscompositional in the structure of processes and works purely on the syntax of processes. It consists of applying a sequence ofreductions, each of which only takes into account the top-level operator of the process. A reduction transforms a satisfaction problem for a composite process into equivalent satisfaction problems for the immediate subcomponents. Using process variables, systems with underfined subcomponents can be defined, and given an overall requirement to the system,necessary and sufficient conditions on these subcomponents can be found. Hence the process variables make it possible to specify and reason about what are often referred to ascontexts, environments, andpartial implementations. Since reductions are algorithms that work on syntax, they can be considered as forming a bridge between traditional noncompositional model checking and compositional proof systems.