基于时序描述逻辑的Web服务本体语言过程模型语义

针对Web服务本体语言(OWL-S)过程模型存在动态交互和时序特征表达能力不足的问题,提出一种基于时序描述逻辑的过程模型形式化方法。通过对OWL-S过程模型的原子过程和组合过程语义进行形式化的描述,得到了OWL-S的过程模型的动态语义,最终实现了对OWL-S过程模型的形式化建模。实例结果验证了所提方法的可行性,为进一步的分析和验证提供了基础。     

OWL-S过程模型的一阶动态逻辑语义研究

针对Web服务本体语言(OWL-S)过程模型语义不完善、难以对其进行有效形式化分析和验证的问题,提出一种OWL-S过程模型的形式化方法。该方法对原子过程提供的输入、输出参数、前提条件、执行效果,以及组合过程控制构造子的语义进行描述,从而得到过程模型的一阶动态逻辑语义。实例结果验证了该方法的有效性。     

OWL-S模型转化为重写逻辑模型的方法

OWL-S模型在基于服务的软件设计中具有重要作用,但由于其非完全形式化的模型,不能直接对其进行形式化分析与验证。基于OWL-S模型的重写逻辑语义框架,通过对数据类型、表达式、控制结构与Process的转换,设计并实现了OWL-S模型到重写逻辑模型的自动转化工具,为能够在软件实现前为设计模型的形式化分析与验证,以及可靠性分析提供基础。     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

模型驱动架构的语义组合Web服务的验证

针对语义Web服务的组合与验证问题,提出了基于模型驱动架构（MDA）的组合方法与基于语义匹配度的匹配方法。组合方法使用UML类图和用例图对OWL-S进行静态组合建模,使用活动图对OWL-S进行动态组合建模。在建模过程中使用基于语义匹配度的匹配方法,选择可用的子Web服务确定最合适的组合Web服务,并将该组合UML模型转化为可验证的Promela语言,使用SPIN工具进行验证,通过验证的UML模型作为模板保存于本体的知识库中以便使用。该模型提高了开发语义Web服务的效率,保证了组合过程的正确性,还能利用模板与语义匹配度实时发现与选择可用的Web服务。     

基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.     

基于Pi演算的OWl-s的Web服务的自动组合

Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型可以用来检查、验证Web服务组合以保证组合的正确性。针对目前最主要的一种语义Web服务组合的规范WEB本体论语言(Ontology Web Langage-Semantic,简称OWL-S),给出基于Pi演算的形式化描述,定义了Pi演算和OWl-S之间的概念映射,并给出了OWl-S的基于Pi演算的形式化模型,最后通过一个案例给出了模型验证的方法。     

基于扩展CPN的OWL-S过程语义建模及分析方法研究

OWL-S过程语义的建模与分析是语义Web服务相关领域需要重点研究的问题。分析了目前OWL-S过程语义研究中存在的问题,提出了一种扩展的着色Petri网PM_ net(过程模型网,Process Model net)来对OWL-S的过程语义进行转化与分析。结合OWL-S过程模型元素的特点,PM_ nct对基本着色Pctri网的变迁和触发规则进行了扩展,使OWL-S的原子过程、组合过程和数据流等核心元素能够等价映射到PM net。同时说明了如何基于PM_ net对OWL-S的过程语义一致性进行分析,为OWL-S本体演化、语义Web服务组合和验证提供了合理的理论基础。     

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

基于答案集的Web服务组合验证

语义Web服务组合的形式化描述和验证,是保证组合服务能正确运行的重要前提基拙。首先描述基于答案集编程(Answer Set Programming)的OWL-S建模方法,并分析基于答案集编程建模的优势。然后给出OWL-S流程模型中几种控制结构到中间模型Petri网的映射,并提出由Petri网生成答案集编程的算法。同时将时态约束引入到 组合服务验证中,利用时态约束表达待验证性质,将验证问题转换为求解逻辑程序的答案集。最后通过一个具体的实例说明该方法的有效性。     

OWL-S的形式语义

本文分析了目前语义Web服务的研究现状和存在的问题,特别是语义web服务描述本体OWL-S的形式语义研究中存在的问题,在Srini Narayanan等人研究的基础上,用情景演算理论进一步研完了OWL—S中组合服务描述的形式语义,从而完善了OWL—S的形式语义,为语义Web服务提供了合理的理论基础。     

Concurrency and Refinement in the Unified Modeling Language

This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models – suitable combinations of diagrams – and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.     

A semantics for Behavior Trees using CSP with specification commands

In this paper we give a formal definition of the requirements translation language Behavior Trees. This language has been used with success in industry to systematically translate large, complex, and often erroneous requirements documents into a structured model of the system. It contains a mixture of state-based manipulations, synchronisation, message passing, and parallel, conditional, and iterative control structures. The formal semantics of a Behavior Tree is given via a translation to a version of Hoare’s process algebra CSP, extended with state-based constructs such as guards and updates, and a message passing facility similar to that used in publish/subscribe protocols. We first provide the extension of CSP and its operational semantics, which preserves the meaning of the original CSP operators, and then the Behavior Tree notation and its translation into the extended version of CSP.     

工作流建模语言XPDL到CSP进程的转化研究

针对工作流定义标准语言XPDL缺乏形式化语义,提出了将XPDL描述转化为通信顺序进程(CSP)的方法,从而可以利用进程代数CSP理论以加强对工作流模型的语义描述分析检测。通过实例分析具体说明转化方法的有效性。     

Specification, Refinement and Verification of Concurrent Systems—An Integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to be used directly within the CSP part of the specification.In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used for the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the CSP operators together with the logic for Object-Z.     

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