基于π演算的反射式需求规约描述方法

目前,大多数学者都意识到需求演化的重要性,然而依然缺乏有效的方法指导需求演化。反射式需求规约通过描述支持OWL-S需求规约演化的元信息,并支持以合理的方式使用这些元信息,实现OWL-S需求规约的演化。本文提出了一种基于π演算的反射式需求规约演化模型,使得反射式需求规约的演化能够以一种正确的方式实现。针对OWL-S需求规约的特点,给出了OWL-S需求规约的π演算描述方法;使用高阶π演算的进程传递机制,描述了支持演化的反射式需求规约;给出了反射式需求规约演化正确性的推理与验证方法。同时,我们采用交通出行的例子论证了本文的观点。     

一种面向动态软件体系结构的在线演化方法

为适应计算环境和用户需求在系统运行期间的变化,满足软件系统进行动态演化的需求,提出面向动态软件体系结构的在线演化方法,设计并实现了一种运行时刻的软件体系结构元模型,将原先运行时刻不可见的体系结构设计信息具体化为显式的体系结构实体,并与系统实现及系统规约之间保持因果关联.元模型的演化可通过反射实现对运行系统的修改和对规约的更新,所有演化行为都在良定义的体系结构元模型的指导下规范地进行,保证了演化前后系统的一致性、完整性和演化的可追溯性.基于该方法开发了可视化支撑平台Artemis-ARC系统,支持构件和服务的设计、开发、集成及动态演化,并通过简单的应用实例展示了在线演化的效果.     

一种形式化的软件可演化性特征描述方法

软件系统的活性和安全性是判断软件可演化性的重要依据之一。现有方法多使用经典逻辑对系统的活性和安全性进行刻画。环境及涉众的复杂性使得软件的可演化性分析可能出现矛盾的输入。经典逻辑的无矛盾律导致其不能对软件系统的演化特性进行有效建模。针对该问题,提出了一种形式化的软件可演化性特征描述方法,该方法允许矛盾性输入的存在,可用于对软件可演化性等存在矛盾特性的系统进行建模和分析。该方法使用多值时序逻辑刻画软件系统的演化需求,同时提出了一种抽象软件模型对软件系统进行建模,通过抽象软件模型的活性和安全性来对软件系统的可演化特征进行描述。     

一种基于智能体技术的软件自适应动态演化机制

针对分布式软件系统在动态演化中面临的原有软件单元难以重用、忽视软件内部运行状态引发的演化需求等问题,借助智能体(agent)具有的环境适应性、变化敏感性等特征,提出了一种基于智能体技术的软件自适应动态演化机制.通过将软件单元封装为Agent,并定义单元间的演化规则,使演化机制重用原有软件单元.通过一种基于数据推送的动态环境感知方法实现Agent间协作关系调整,同时满足来自内外部环境引发的动态演化需求.通过引入信息中介服务,实现了基于改进合同网的Agent协作策略,能够自适应地更替Agent,满足用户意愿变更引发的动态演化需求.依据演化机制在支撑环境中的运行情况及相关能力指标的分析,说明所提出的演化机制适用于动态复杂的分布式软件系统,是一种有效的软件自适应动态演化机制.     

面向开源软件的演化确认方法

软件演化确认是软件工程领域的一个重点和热点的研究方向。由于开源软件具有群智开发,演化过程不可控和不可建模等特点,使得传统的确认方法不适合于开源软件,故从功能语义角度提出了一种软件演化确认方法,试图将代码按主题的方式进行聚类,每一个主题表征软件系统的一个功能集合,演化确认工作被转化为功能集合与演化需求之间的映射关系。通过对现有开源软件的源代码进行实验,获取了大量的真实可靠实验数据,对这些实验数据进行分析后得出的实验结果表明该方法相较基于文本的基线方法,更能有效区分是否已经演化,可以用于对软件演化进行确认工作。     

支持动态演化的开放构件模型及其设计规范

针对开放系统演化的技术需求,提出一种具有良好的构造性和演化性的开放构件模型——SMC。SMC由服务接口、构件体和管理外壳组成,构件体可层级嵌套子构件,其管理外壳以松耦合方式提供一组涵盖反射、上下文感知和动态配置等在线演化原语的元接口。在SMC形式化定义的基础上,给出基于OMG IDL描述的元接口设计规范。分析结果表明,SMC能显式支持动态演化。     

一种基于模糊概念格和代码分析的软件演化分析方法

软件系统的演化分析是程序分析和程序理解的一个重要方面.通过演化分析可以了解系统需求和设计的演化趋势,从而更好地理解系统的需求和设计决策.文中在前期工作所提出的基于模糊概念格的程序分析方法基础上,进一步将其用于系统演化分析,提出了一种基于模糊概念格的软件演化分析方法.该方法利用基于概念相似度度量的松弛树匹配的方法建立不同版本概念格中概念和概念子格之间的映射关系,在此基础上通过结构差异分析来发现各种演化类型.实验表明,该方法能够有效地发现不同版本之间的高层演化信息,有助于开发人员理解系统的演化历史以及相关的设计决策.     

工业复杂软件系统的成长性构造框架与实现

工业领域中智能制造和智慧城市的快速发展,促使各种具有边界开放、持续演化、自适应性等特征的复杂软件系统的出现。基于还原论和单一组织的传统软件开发方法不再适合发展需求,也不能满足跨组织的社会化协作和资源共享等基本需求。本文提出一种基于容器云和跨组织资源共享的复杂软件系统成长性构造框架,通过容器技术、多租户技术、信息资源目录技术实现社会化协作开发和复杂软件系统成长性构造,并且该框架在一个工业研究案例中的应用实践证明了其在复杂软件系统的快速构建和演化方面具有重要意义。     

基于动态构件框架的构件演化

软件系统是对现实世界模型的反映,现实世界的变化要求软件系统进行相应的演化。软件演化是软件系统的动态行为,贯穿整个软件生命周期,从系统的初始开发阶段到最终的软件维护。软件演化包括软件系统的过程、方法、技术、组织方式等的演化。基于软件构架和构件的开发方法实现的系统比传统的开发方法具有更好的易演化性。软件构架高度抽象地描述了软件系统的结构,包括系统元素的描述、元素之间的交互、用于指导元素复合的模式和这些模式的约束。我件是组成构架的基本元素,是对系统应用功能的实现;构件封装了功能性,有着自己的内部状态信息;构件的实现是异质的（可以用多种语言实现）,而且在系统实现中可能使用的是第三方提供的构件。基本构架和构件的系统可以有两种方式的演化：一是整体构架的演化,重组系统的构架,增加、删除系统的构件,修改构件之间的拓扑结构;二是系统中单个构件的演化,着眼于系统的单个构件,修改构件的接口、功能。本文着重于研究构架构件系统中构件的演化,对系统使用的构件进行演化,在不修改系统中其他的构件,保持构件之间的基本连接拓扑结构不变的情况下,将演化后的构件替换系统中的原有构件,实现对系统功能的修改。     

基于层次着色Petri网的需求工程过程框架

提出一种基于层次着色Petri网的需求工程过程框架,对软件需求工程过程、需求活动、需求任务及其功能进行了形式化定义,为软件需求工程实现了一个清晰、完整、无二义性的精确描述框架,并为最终产生高质量的软件需求规格说明奠定了坚实的基础,也为软件需求的精化、规约、复用、演化以及需求管理、需求质量控制、度量等提供了严格数学依据。     

面向媒体时序描述的带时间自动机的自动构造方法

依据有穷状态自动机模型,面向程序规范的并发系统和分布式系统测试方法的研究已经取得许多结果。由于特殊的实时和同步要求,这些结果不能直接应用于分布式多媒体软件系统的测试。为此,作者提出一种面向媒体对象时序描述的地间自动机（Ｔｉｍｅｄ ａｕｔｏｍａｔａ）的自动构造方法,根据带时间自动机,对分布式多媒体软件系统进行非确定性测试时,可以较容易地判断运行结果正确与否;在进行确定性测试时,可以辅助自动生成测试用     

Intelligent support for specifications transformation

The authors describe an expert system, the Specification-Transformation Expert System (STES), which is to translate requirements specifications into design specifications automatically during the development phase of the software life cycle. STES accepts as input a software-requirements specification expressed in terms of dataflow diagrams. Using rules that embody a structured design methodology, STES translates this specification into a template describing a structure chart. STES consist of a knowledge base and an inference engine. The knowledge base contains information on the structured-design methodology and heuristic guidelines to help determine when certain methods should be applied. Given a target software system's requirements specification, the STES inference engine can perform intelligent decision-making and determine a suitable architectural design specification for the software system being designed. STES was originally implemented in OPS5 on a VAX11/780 computer. It has since been ported to an Apollo DN 3000 workstation and integrated with a commercial CASE tool     

需求工程在南京地铁企业信息化建设中的应用

高质量的需求规范是高质量软件制品的必要条件;对需求获取、需求规范的定义、需求验证和评审、需求信息的传递、需求的进化和演变等需求工程中基本活动进行了实践和总结。     

Model checking large software specifications

In this paper, we present our experiences in using symbolic model checking to analyze a specification of a software system for aircraft collision avoidance. Symbolic model checking has been highly successful when applied to hardware systems. We are interested in whether model checking can be effectively applied to large software specifications. To investigate this, we translated a portion of the state-based system requirements specification of Traffic Alert and Collision Avoidance System II (TCAS II) into input to a symbolic model checker (SMV). We successfully used the symbolic model checker to analyze a number of properties of the system. We report on our experiences, describing our approach to translating the specification to the SMV language, explaining our methods for achieving acceptable performance, and giving a summary of the properties analyzed. Based on our experiences, we discuss the possibility of using model checking to aid specification development by iteratively applying the technique early in the development cycle. We consider the paper to be a data point for optimism about the potential for more widespread application of model checking to software systems     

反射式集成框架的规约描述方法研究

反射式集成框架的规约描述方法,主要研究在分布式实时应用领域基于构件的软件开发模式中集成框架的形式化规约描述问题.这种描述方法通过引入反射技术,除了描述集成框架中组成要素的业务逻辑之外,还对各要素的实时性能约束、运行时状态的变化以及可能具有的需求变更等特征进行形式化规约,从而支持软件在需求分析阶段的演化进程,并以指导与实现实时应用软件开发时业务逻辑与系统非功能性特征的关注分离.     

化学抽象机的分析与应用研究

1 引言化学抽象机形式化语言(CHAM:the Chemical Abstract Machine)最早是由法国科学家Gerard Berry和Gerard Boudol提出来的,它主要用于异步并行计算模型的建模,通过把化学反应和抽象机的概念有机地结合来描述系统状态的变化。它把一个系统的状态看成化学溶液,溶液由分子组成,分子根据一定的反应规则相互反应又引起新的系统状态变化。溶液中不同的分子可以按照反应规则平行地进行反应,只要各自反应的分子集不重叠。由于CHAM在描述系统动态     

Property transformation under specification change

Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification toward an implementation, they are also required in response to changes in requirements, or to incorporate different aspects of the system, e.g., fault tolerance or timing, initially ignored in order to simplify reasoning. This paper presents an approach for evolving Z specifications by the step-wise application of a number of simple rules. These rules not only document the evolution of the specification, but also make precise how properties of the system evolve with the specification. Hence, reasoning about these properties performed on the original specification need not be repeated on the new specification.     

Using abstraction and model checking to detect safety violations inrequirements specifications

Exposing inconsistencies can uncover many defects in software specifications. One approach to exposing inconsistencies analyzes two redundant specifications, one operational and the other property-based, and reports discrepancies. This paper describes a “practical” formal method, based on this approach and the SCR (software cost reduction) tabular notation, that can expose inconsistencies in software requirements specifications. Because users of the method do not need advanced mathematical training or theorem-proving skills, most software developers should be able to apply the method without extraordinary effort. This paper also describes an application of the method which exposed a safety violation in the contractor-produced software requirements specification of a sizable, safety-critical control system. Because the enormous state space of specifications of practical software usually renders direct analysis impractical, a common approach is to apply abstraction to the specification. To reduce the state space of the control system specification, two “pushbutton” abstraction methods were applied, one which automatically removes irrelevant variables and a second which replaces the large, possibly infinite, type sets of certain variables with smaller type sets. Analyzing the reduced specification with the model checker Spin uncovered a possible safety violation. Simulation demonstrated that the safety violation was not spurious but an actual defect in the original specification