基于进程代数的安全软件体系结构建模

分析了基于进程代数的软件体系结构模型的安全性,将相容性检查和互操作性检查从单个软件体系结构推广到不同风格的体系结构风格,扩展基于进程代数的软件体系结构描述语言,通过顺序进程代数项族和预定义的体系结构类型调用对软件体系结构安全建模。通过一个例子介绍了这种建模方法。     

基于代数的软件过程建模系统的设计与实现

软件过程建模的主要目的是建立组织内软件开发过程的模型,使得软件开发过程在整个组织内获得一致的理解,进而提高软件开发效率和改进软件生产质量.软件过程建模语言一方面要易于理解、具有较强的表达能力,同时也要易于分析和验证,以保证所要描述的软件过程的正确性.介绍了基于代数的软件过程建模系统ASPMS的设计和实现,该系统提供了图形化的建模表示方式,而该图形化表示方式具有基于多元π演算的形式化语义,从而较好地平衡了建模语言的易于理解、具有较强的表达能力和易于分析和验证这一矛盾的内在要求.     

C-programs verification based on mixed axiomatic semantics

The mixed axiomatic semantics of the C-kernel language is described. This language is the kernel of a representative subset which is called C-light. Such semantics makes possible for the verification conditions to be simplified in many cases. The semantics is the basis of the verification conditions generator for C-kernel programs. An example illustrating the application of the inference rules of the semantics is considered.     

基于系统理论过程分析的安全关键软件安全性验证方法

现代安全关键系统的功能实现越来越依赖于软件,这导致软件的安全性对系统安全至关重要,而软件的复杂性使得采用传统安全性分析方法很难捕获组件交互过程带来的危险。为保证安全关键系统的安全性,提出一种基于系统理论过程分析（STPA）的软件安全性验证方法。在安全控制结构基础上,通过构建带有软件过程模型变量的过程模型,细化分析危险行为发生的系统上下文信息,并以此生成软件安全性需求。然后通过设计起落架控制系统软件,采用模型检验技术对软件进行安全性验证。结果表明,所提方法能够在系统级层面有效识别出软件中潜在的危险控制路径,并可以减少对人工分析的依赖。     

Compositional and holistic quantum computational semantics

In quantum computational logic meanings of sentences are identified with quantum information quantities: systems of qubits or, more generally, mixtures of systems of qubits. We consider two kinds of quantum computational semantics: (1) a compositional semantics, where the meaning of a compound sentence is determined by the meanings of its parts; (2) a holistic semantics, which makes essential use of the characteristic “holistic” features of the quantum-theoretic formalism. We prove that the compositional and the holistic semantics characterize the same logic.     

一种弹性的软件过程模型验证工具

过程模型验证是保证软件过程定义正确性的重要手段.针对目前过程模型验证中的一些问题,首先提出了一种以活动为中心的软件过程元模型,并以XML对其进行描述.在此基础上,从行为、资源、组织视图结合的角度,提出了保证软件过程模型正确性的语义约束规则.最后,提出了一种弹性的用于验证XML描述的过程模型的机制,并基于此实现了过程模型验证工具,来验证过程模型的正确性.     

From individuals to populations: A mean field semantics for process algebra

A new semantics in terms of mean field equations is presented for WSCCS (Weighted Synchronous Calculus of Communicating Systems). The semantics captures the average behaviour of the system over time, but without computing the entire state space, therefore avoiding the state space explosion problem. This allows easy investigation of models with large numbers of components. The new semantics is shown to be equivalent to the standard Discrete Time Markov Chain semantics of WSCCS as the number of processes tends to infinity. The method of deriving the semantics is illustrated with examples drawn from biology and from computing.     

Automatic verification of distributed systems: The process algebra approach

A survey of tools for the analysis of distributed systems represented through process algebras is presented. The tools are compared with respect to a set of qualitative parameters. From this analysis, the properties which are desirable for concurrency tools are investigated. Criteria to evaluate the suitability of a tool with respect to a particular user are proposed.     

Compositional semantics and behavioral equivalences for P Systems

The aim of the paper is to give a compositional semantics in the style of the Structural Operational Semantics (SOS) and to study behavioral equivalence notions for P Systems. Firstly, we consider P Systems with maximal parallelism and without priorities. We define a process algebra, called P Algebra, whose terms model membranes, we equip the algebra with a Labeled Transition System (LTS) obtained through SOS transition rules, and we study how some equivalence notions defined over the LTS model apply in our case. Then, we consider P Systems with priorities and extend the introduced framework to deal with them. We prove that our compositional semantics reflects correctly maximal parallelism and priorities.     

Using a process algebra interface for verification and validation of UML statecharts

UML diagrams are the conventional methods for visual modeling systems. Among them, the Statechart diagrams are used to show the runtime behavior of a system, but the correctness of such diagrams is the primary concern of the designers because of concurrency issues like livelock, inaccessible states, and non-deterministic states. Process algebra methods have the capabilities that are suitable for verification and validation of Statecharts. To this end, in this paper, process algebra language LOTOS (Language Of Temporal Ordering Specification) is used as the target language, and a method is presented to map UML Statecharts to the LOTOS processes, called USLP. Then the correctness of the proposed mappings is proved by demonstrating the isomorphism relation between the Labeled Transition System (LTS) of a Statechart and the LTS of its transformed LOTOS specification. Next, tools CADP (Construction and Analysis of Distributed Processes) is used for verification and validation of the mapped LOTOS models, and the CSP process algebra and its tools, FDR are used to verify the properties could not be verified by the LOTOS and its toolset. The experimental results show our approach can: (1) verify some properties (the issues) that are not verified by other approaches and (2) reduce the space that should be searched to verify the properties.     

Correctness of the compiling process based on axiomatic semantics

Summary A language that includes computed gotos and parameterized procedures is defined and its semantics are given axiomatically. A number of program transformations are described and proved correct. Taken collectively and applied repeatedly these transformations compile the full language into a low level subset.     

基于进程代数的网络体系结构形式化模型

首先用形式化方法给出了网络实体、网络连接件和网络体系结构框架模型的定义,然后利用进程代数理论定义了网络体系结构上的网络实体运算,进而建立了网络体系结构的代数模型,为进一步研究网络体系结构打下了坚实的理论基础。     

一个支持软件需求验证的过程模型研究

需求验证是软件需求阶段的一个重要环节,未经验证的需求给项目成功带来较大的需求风险。在前期研究的基础上,从需求验证的基本原理和可操作性出发,提出一个支持需求验证的过程模型(RVPM),进行形式化描述,并论述了需求验证过程的几个关键过程和策略。结合实例,分析了如何应用该模型来指导需求验证过程。理论和实例分析表明：该模型有效地克服了需求验证过程的复杂性和经验操作,有效降低项目需求风险。     

基于软硬件协同形式验证的固件漏洞分析技术

为了系统高效地分析固件中潜在的安全隐患,提出了一种基于行为时序逻辑 TLA 的软硬件协同形式验证方法。通过对固件工作过程中的软硬件交互机制进行形式建模分析,在动态调整攻击模型的基础上,发现了固件更新过程中存在的安全漏洞,并通过实验证实了该漏洞的存在,从而证明了形式验证方法的可靠性。     

基于委托-代理模型的施工过程成本博弈

施工项目管理者的成本控制目标是,通过激励契约达到成本控制要求,提高成本控制效率.但是管理者运用激励机制控制单位产品成本具有片面性,没有考虑工人为了提高成本控制效率需要付出一定的精力和时间,从而影响其收益以及降低生产成本的积极性,因此,管理者和工人会围绕产品成本降低产生的收益分配形成动态成本博弈.对此,提出建设项目背景下基于单位时间的委托代理模型.通过分析发现:工人努力程度与激励系数呈非线性正相关;在一定范围内,工人的收益会随着努力程度的提高先增加并达到峰值后再减少;在工人努力程度达到最优时,管理者的收益会随激励系数的提高而增加并达到峰值.通过设置合理的激励系数能使管理者和工人的收益达到最优.最后以钢筋制作搭接工序为例,分析模型的可行性.     

基于小型软件企业的软件过程改进模型的研究

软件过程改进是小型软件企业提高软件质量和生产率的必经之路.文章分析了集成软件能力成熟度模型CMMI、个体软件过程PSP和群组软件过程TSP三者之间的关系,并结合我国小型软件企业的特点,提出了一种适用于小型软件企业的过程改进模型.     

The semantics and verification of timed service choreography

As a service composition and coordination language, the service choreography gives the global and neutral view on the collaboration among a collection of highly distributed services involving multiple different organizations or heterogeneous independent processes. In this paper, we extend the service choreography by introducing the explicit time activity, which can be used to specify and reason about the timed behaviour of Web service choreography. Then we explore an execution model for the proposed timed service choreography which possesses several novel features, such as timed activity, choreography composition, exception handling and finalization. Furthermore, a set of mapping rules is elaborately designed to translate the timed choreography into communicating sequential programs processes, thus the corresponding simulation and verification of Web services choreographies with timing restrictions can be carried out in the model checker process analysis toolkit. The case study shows that our approach is both effective and practical.     

基于CMMI的软件过程改进研究

随着软件过程管理概念的普及推广，软件业界对软件过程改进的讨论很多。由于这些讨论大多集中在工程管理的具体技术及工具应用，因而对软件过程框架特性未形成统一的认识。针对软件过程的实际使用，阐述了软件过程改进框架的基本思想，分析了软件过程改进和评估中的关键问题，为其应用提供了参考思路。     

基于度量的软件过程改进研究

在软件开发的整个过程中,需要对各个阶段进行评估、分析、改进,它们是一个不断循环的过程.即软件过程改进贯穿于软件开发的始终.如何对软件过程进行度量、度量元是什么,已经成为当前国内外研究的热点.对当前国内许多机构开展的质量管理体系认证模型进行研究,提出了一种基于CMMI的6σ软件度量框架,在此基础上分析了软件过程改进和评估中的关键问题.通过对软件过程的改进,从而提高软件产品质量和提升软件开发效率.