Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.     

A UML-based static verification framework for security

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.     

Relating evolving business rules to software design

In order to remain useful, it is important for software to evolve according to the changes in its business environment. Business rules, which can be used to represent both user requirements and conditions to which the system should conform, are considered as the most volatile part in today's software applications. Their changes bring high impact on both the business processes and the software itself. In this paper, we present an approach that considers business rules as an integral part of a software system and its evolution. The approach transcends the areas of requirements specification and software design. We develop the Business Rule Model to capture and specify business rules, and the Link Model to relate business rules to the metamodel level of software design elements. The aim is to improve requirements traceability in software design, as well as minimizing the efforts of software changes due to the changes of business rules. The approach is demonstrated using examples from an industrial application.     

Managing Software Requirements Changes Based on Negotiation-Style Revision

For any proposed software project,when the software requirements specification has been established,requirements changes may result in not only a modification of the requirements specification but also a series of modifications of all existing artifacts during the development.Then it is necessary to provide effective and flexible requirements changes management.In this paper,we present an approach to managing requirements changes based on Booth’s negotiation-style framework for belief revision.Informally,we consider the current requirements specification as a belief set about the systemto-be.The request of requirements change is viewed as new information about the same system-to-be.Then the process of executing the requirements change is a process of revising beliefs about the system-to-be.We design a family of belief negotiation models appropriate for different processes of requirements revision,including the setting of the request of requirements change being fully accepted,the setting of the current requirements specification being fully preserved,and that of the current specification and the request of requirements change reaching a compromise.In particular,the prioritization of requirements plays an important role in reaching an agreement in each belief negotiation model designed in this paper.     

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     

一个面向网络并行环境的需求规约语言

提出了一个面向网络并行环境的需求规约语言ＯＯＲＳＬ。ＯＯＲＳＬ支持面向对象的分析方法,可以定义并行成分一进程,可以使用前后断言来表达用户的功能需求,允许将非经和半形式化的需求定义嵌入形式化的需求定义中。因此,ＯＯＲＳＬ语言是一个半形式化的语言,它为网络并行环境下的软件自动化和软件形式化开发提供了支持介绍了ＯＯＲＳＬ的设计思想和主要语法成分。给出了一个实例。     

An intelligent assistant for requirements validation

The process of determining user requirements for software systems is often plagued with uncertainty, ambiguity, and inconsistency. Rapid prototyping offers an iterative approach to requirements engineering that can be used to alleviate some of the problems with communication and understanding. Since the systems development process is characterized by changing requirements and assumptions, involving multiple stakeholders with often differing viewpoints, it is beneficial to capture the justifications for the decisions in the development process in a structured manner. Thisdesign rationale captured during requirements engineering can be used in conjunction with the rapid prototyping process to support various stakeholders involved in systems development. CAPS (the Computer Aided Prototyping System) has been built to help software engineers rapidly construct prototypes of proposed software systems. REMAP (Representation and MAintenance of Process knowledge) provides a conceptual model and mechanisms to represent and reason with (design) rationale knowledge. In this paper, we describe how in the context of evolving requirements, the CAPS system augmented with REMAP helps firm up software requirements through iterative negotiations via examination of executable prototypes and reasoning with design rationale knowledge.     

基于设计模型的信息系统自动测试方法

针对当前自动测试领域存在的问题,提出了一种基于设计模型的自动测试方法（Model Based Automated TestIng System,MATIS）。该方法利用用户界面自动生成方法,把设计模型中的类属性定义和实现中的控件属性组织在一起,构建描述界面的逻辑对照表,辅助测试脚本引擎执行自动测试脚本。借助设计模型中扩展的类定义,MATIS方法可以自动生成测试用例和测试数据。MATIS方法是一个较轻量级的方法,更贴近于实际的软件开发过程,可以有效地降低自动测试成本。     

The impact of requirements changes on specifications and state machines

Requirements change both during and after a phase of development for a variety of reasons, including error correction and feature changes. Requirements change management is one of the most complex and difficult problems to deal with in requirements elicitation and tracking. It is generally not understood how a specific change propagates through the specification and into the code. In this paper we capture requirements changes as series of atomic changes in specifications. Using a rigorous specification method called sequence‐based specification, we propose a set of algorithms for managing all possible atomic requirements changes. The algorithms have been formulated within an axiom system for sequence‐based specification and proven for correctness. They have also been implemented in a prototype tool 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. The approach of utilizing state machines to model and manage requirements changes guarantees strong evidence about the correctness and completeness of the proposed theory that will lead to more reliable software in the presence of change, especially with embedded systems and safety‐critical systems. The solution described is general enough for adoption by software and system developers, and well suited for incremental development. Copyright © 2008 John Wiley & Sons, Ltd.     

A two‐step methodology to reduce requirement defects

Defects are introduced into a software product during every phase of software development. A major source of defects that is often overlooked is requirements generation. Requirement errors discovered in later phases of the software development process are the most costly to correct because all phases of software development are usually impacted. Requirement defects can be categorized into two main types: 1) specification generation errors; and 2) unwanted/unnecessary/incorrect user functionality. This experience report presents the results of incorporating a two‐step methodology which combines Operational Demonstrations of the user interface and Requirement Inspections on software requirement specifications. The two‐step methodology addresses and corrects both types of requirement defects. Results from this experience support the premise that cost reduction and quality improvement can be obtained using a combined Operational Demonstration and Requirement Inspection development methodology for software requirements.     

Dialogue modelling of graphical user interfaces with a production system

In systems development it is essential for a piece of software to be able effectively to incorporate the requirements of the particular task domain that it is intended to address. This paper describes an approach that uses dialogue modelling to carry the requirements derived from task analysis through to the implementation phase of development. A notation based on production systems is used to develop an abstract specification of user and system behaviour which can subsequently be used as the basis for the implementation. The requirements for a computer-based tool are also discussed, with particular attention being given to ways in which the communication and reasoning about such a dialogue design can be supported.     

基于企业流程的需求形式化验证技术

需求验证是为了确保需求规格说明具有良好特性(完整性、一致性、无二义性)而对需求规格说明进行的一种审查活动。目前广泛使用的需求验证技术存在着两个问题:难以处理大型、复杂的需求文档;审查过程需要相当长的时间。该文所研究的基于企业流程的需求形式化验证技术,通过对需求文档中企业流程各活动之间的逻辑关系进行验证,从而发现其中的不一致性和二义性。     

Integration of informal and formal development of object-oriented safety-critical software

The KeY system allows for the integrated informal and formal development of object-oriented Java software. In this paper we report on a major industrial case study involving safety-critical software for the computation of a particular kind of railway timetable used by train conductors. Our case study includes formal specification of requirements both on the analysis and the implementation level. Particular emphasis in our research is placed on the challenge to make authoring and maintenance of formal specifications easier. We demonstrate that the technique of specification patterns as implemented in KeY for the language OCL yields significant improvements.     

基于模型设计的列车网络控制逻辑开发研究

现代轨道交通列车控制系统的结构日益复杂,针对目前列车网络控制逻辑开发中存在复杂度和开发难度大的问题,详细研究了基于模型设计高效率开发列车控制单元逻辑软件的方法。通过创建技术需求规范、生成定点模型、自动生成产品级软件代码和持续不断的测试及验证,实现了机车辅助变流器负载控制逻辑的开发。离线仿真试验和地面联调试验结果表明本方法可实现机车辅助变流器负载分配规则和逻辑需求,证明了基于模型设计方法在整车控制单元软件开发工程应用中的有效性和可行性,为轨道交通列车其他控制单元的软件高效率开发提供参考。     

χSuds-SDL: A Tool for Testing Software Architecture Specifications

Available statistical data shows that the cost of repairing software faults rises dramatically in later development stages. In particular, the new technology of generating implementation code from architectural specifications requires highly reliable designs. Much research has been done at this stage using verification and validation techniques to prove correctness in terms of certain properties. A prominent approach of this category is model checking (Atlee, J.M., and Gannon, J. 1993. State-based model checking of event-driven systems requirements. IEEE Trans. Software Eng., 19(1): 24–40.) Such approaches and the approach of software testing are complementary. Testing reveals some errors that cannot be easily identified through verification, and vice versa. This paper presents the technology and the accompanying tool suite to the testing of software architecture specifications. We apply our state-of-the-art technology in software coverage testing, program diagnosis and understanding to software architectural designs. Our technology is based on both the control flow and the data flow of the executable architectural specifications. It first generates a program flow diagram from the specification and then automatically analyses the coverage features of the diagram. It collects the corresponding flow data during the design simulation to be mapped to the flow diagram. The coverage information for the original specification is then obtained from the coverage information of the flow diagram. This technology has been used for C, C++, and Java, and has proven effective (Agrawal, H., Alberti, J., Li, J.J., et al. 1998. Mining system tests to aid software maintenance, IEEE Computer July, pp. 64–73.)     

Experience on knowledge-based software engineering: A logic-based requirements language and its industrial applications

A formal requirements specification language plays an important role in software development. Not only can such language be used for stating requirements specification, but also can be used in many phases of software development life cycle. The FRORL project started from constructing a language with a solid logical foundation and further expanded to research in verification, validation, requirements analysis, debugging, and transformation. Research in this project aided in some industrial applications in which a code generation tool produced software for embedded systems. This article reports the experiences gained from this project and states the value of research in knowledge-based software engineering.     

4—5GHz低噪声放大器模块设计

根据低噪声放大器（LNA）的性能指标要求,首先介绍了LNA结构选取,再从器件和介质板的选择,输入输出匹配,稳定性和偏置电路等方面介绍了LNA的设计,并且利用微波仿真软件Serenade8．7对LNA电路进行了仿真和优化设计,给出仿真结果。最后给出的实际测试结果表明,该LNA能够满足指标要求。