Pushing requirements changes through to changes in specifications

Requirements changes can occur both during and after a phase of development for a variety of reasons, including error correction and feature changes. It is difficult and intensive work to integrate requirements changes made after specification is completed. Sequence-based specification was developed to convert ordinary functional software requirements into complete, consistent, and traceably correct specifications through a constructive process. Algorithms for managing requirements changes meet a very great need in field application of the sequence-based specification method. In this paper we propose to capture requirements changes as a series of atomic changes in specifications, and present polynomial-time algorithms for managing these changes. The algorithms are built into the tool support with which users are able to push requirements changes through to changes in specifications, maintain old specifications over time and evolve them into new specifications with the least amount of human interaction and rework. All our change algorithms are supported by rigorous mathematical formulation and proof of correctness. The application example is a safe controller. Software Quality Research Lab, Department of Electrical Engineering and Computer Science, University of Tennessee at Knoxville, http://www.cs.utk.edu/sqrl/     

Automated structural analysis of SCR‐style software requirements specifications using PVS

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)‐style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd.     

应用软件开发的需求风险及控制

在应用软件开发过程中,由于软件需求本身的隐含性、用户与开发者之间的沟通障碍,以及需求随着时间、用户的变化而变更等原因,可能使需求分析偏离实际需求而最终导致软件开发的失败,这种可能性称为需求风险。需求分析是软件开发过程中最初始、最基础的工作,也是最重要的工作之一,其成败将直接并最终决定软件开发的成败,并且呈倍增效应。需求分析的关键是使隐含的需求明确,使变更的需求可控,采用座谈会、需求调查表、需求启发、角色扮演等方法可以使需求明确化;采用面向对象的方法及UML工具、领域专家的全程参与、需求分级、二次开发接口等方法可以使需求变更处于可控范围内。实践证明,这些都是控制需求风险的有效方法。     

基于SWRL的软件需求一致性验证方法

需求质量已经成为确保软件项目成功的一个重要因素,对复杂软件系统的需求进行检查和验证,是需求工程中非常重要的工作。在基于领域本体的需求获取和分析等相关工作基础上,提出了一种基于本体和语义规则的需求一致性验证方法,将自然语言描述的需求分解成若干结构良好的最小需求项,使用领域本体的概念模型对其进行形式化和结构化的表示。通过领域本体中的知识来映射需求语义,采用语义万维网规则语言（SWRL）来定义需求一致性验证的推理规则,并通过实例对此方法进行了分析和验证。     

关于软件需求中的不一致性管理

复杂软件系统开发的一个关键问题是分析和处理可能存在的不一致的需求描述.这个问题解决得好坏直接影响到需求规格说明的质量,进而影响到最终软件产品的质量.在目前公认的一个不一致需求管理框架的基础上,就需求不一致性管理方面的有代表性的工作,进行了较为系统的分析,以期建立对当前需求工程中,关于不一致的需求管理方法和技术的全面认识.最后,对需求不一致性管理方面的研究进行了展望.     

User interface specification with sequence diagrams: an application to the AIRBUS A380 Datalink system

The development of user interfaces for safety critical systems is driven by requirements specifications. Because user interface specifications are typically embedded within complex systems requirements specifications, they can be intractable to manage. Proprietary requirements specification tools do not support the user interface designer in modelling and specifying the user interface. In this paper, a new way of working with embedded user interface specifications is proposed, exploiting sequence diagrams with a hypertext structure for representing and retrieving use cases. This new tool concept is assessed through an application to the requirements specification for the Airbus A380 air traffic control Datalink system; engineers involved in the development of the Airbus cockpit used a prototype of the tool concept to resolve a set of user interface design anomalies in the requirements specification. The results of the study are positive and indicate the user interface to requirements specification tools which user interface designers themselves need.     

A formal framework for ASTRAL intralevel proof obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL specifications. ASTRAL is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering. In this paper, further details of the ASTRAL environment components and the critical requirements components, which were not fully developed in previous papers, are presented. Formal proofs in ASTRAL can be divided into two categories: interlevel proofs and intralevel proofs. The former deal with proving that the specification of level i+1 is consistent with the specification of level i, and the latter deal with proving that the specification of level i is consistent and satisfies the stated critical requirements. This paper concentrates on intralevel proofs     

Round-Trip Prototyping Based on Integrated Functional and User Interface Requirements Specifications

Requirements engineering in the new millennium is facing an increasing diversity of computerised devices comprising an increasing diversity of interaction styles for an increasing diversity of user groups. Thus the incorporation of user interface requirements into software requirements specifications becomes more and more mandatory. Validating these requirements specifications with hand-made, throw-away prototypes is not only expensive, but also bears the danger that validation results are not accurately fed back into the requirements specification. In this paper, we propose an enhancement of the requirements specification method SCORES for an explicit capturing of user interface requirements. The advantages of the approach are threefold. First, the user interface requirements specification is UML-compliant and integrated into the functional requirements specification. Second, prototypes for validation purposes can semi-automatically be generated. Third, the model-based generation of prototypes allows for ‘round-trip prototyping’ such that manual changes of the prototype during the validation process are automatically fed back into the requirements specification.     

智能需求获取与建模研究综述

需求获取和建模是指从需求文本或记录中获取显式和隐式的需求,并通过表格化、图形化、形式化等方法构建相应模型的过程,是软件开发过程中极为关键的一步,为后续系统设计与实现铺平道路,提高软件开发效率和质量,提升软件系统稳定性和可行性.研究者们在需求获取与建模方面获得了一系列研究成果,根据其关注阶段不同,可以将它们分为需求知识提...     

Requirements engineering: making the connection between the software developer and customer

Requirements engineering are one of the most crucial steps in software development process. Without a well-written requirements specification, developer's do not know what to build, user's do not know what to expect, and there is no way to validate that the created system actually meets the original needs of the user. Much of the emphasis in the recent attention for a software engineering discipline has centered on the formalization of software specifications and their flowdown to system design and verification. Undoubtedly, the incorporation of such sound, complete, and unambiguous traceability is vital to the success of any project. However, it has been our experience through years of work (on both sides) within the government and private sector military industrial establishment that many projects fail even before they reach the formal specification stage. That is because too often the developer does not truly understand or address the real requirements of the user and his environment.The purpose of this research and report is to investigate the key players and their roles along with the existing methods and obstacles in Requirements Elicitation. The article will concentrate on emphasizing key activities and methods for gathering this information, as well as offering new approaches and ideas for improving the transfer and record of this information. Our hope is that this article will become an informal policy reminder/guideline for engineers and project managers alike. The success of our products and systems are largely determined by our attention to the human dimensions of the requirements process. We hope this article will bring attention to this oft-neglected element in software development and encourage discussion about how to effectively address the issue.     

浅谈软件项目的需求分析

当今世界各行各业对软件的依赖程度急剧增长,而在规定的时间和预算内开发出可靠并满足用户需求的软件系统,对于许多开发者来说都是一件非常困难的事情。由于软件项目中的需求变更而导致软件项目失败的案例越来越多,所以如何高质量完成需求分析已经被许多软件公司列入了重要的流程化管理中。需求分析的任务还不是确定系统怎样完成它的工作,而仅仅是确定系统必须完成哪些工作,也就是对目标系统提出完整、准确、清晰、具体的要求。     

从用户需求到软件规约：一种问题变换的方法

研究的目的是在获取用户需求和领域描述的基础上规约出对软件规格的描述.提供了一种实现从用户需求到软件规约的平滑和可推理的变换方法.在深入研究问题框架方法的基础上,采用Hoare 的通信顺序进程语言CSP及Lai的最弱环境演算符实现了整个问题图的变换,且导出的软件规格是具有高抽象粒度的程序代码模型,能够被FDR模型检测工具所验证.该工作为实现嵌入式软件开发从需求到软件代码、文档的自动转化及验证等奠定了理论基础.此外,把该理论与模型检测工具FDR联合起来会有助于提高嵌入式软件开发的效率和准确性.     

利用语义模型的需求可跟踪性的实现

需求的可跟踪性——一种可以把需求规格说明和其他在软件系统生命周期产生的产品联系起来的性能，很早就已经广泛地被认为是高效软件工程管理和软件系统质量的关键因素。该文提出了一种基于语义模型的方法，把从需求获取到编辑SRS的这样一个过程划分成若干阶段，并找出每一阶段的语义元素和联系。     

Formalism and Language Tools for Specification of the Semantics of Software Libraries

The paper considers the specification of the structure and the behavior of software libraries. It describes the existing problems of library specifications. A brief overview of the research field concerned with formalizing the specification of libraries and library functions is presented. The requirements imposed on the formalism designed are established; the formalism based on these requirements allows specification of all the properties of the libraries needed for automation of several classes of problems: defect detection in software, migration of applications into a new environment, and generation of software documentation. Requirements for language tools based on the developed formalism are proposed. The conclusion defines potential directions for further research.     

基于UML的软件形式化需求分析与验证

针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言（UML）模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。