Formal specification and design time testing

It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence to the regularity and uniformity hypotheses in dynamic validation. It is shown that such an approach offers positive benefits by providing early design validation and a controlled, disciplined design process     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

Formal Specifications of User Requirements

There is a wide gap between informal requirements and a formal object-oriented specification. To help bridge this gap, we propose that a formal and executable user-centred model should be constructed initially. The user-centred model, which specifies the behaviour that the environment expects from the system, is expressed in terms of agent views and gives very early feedback to the requirements' capture process. Once the user-centred model has been validated with respect to the environment, it can be used as a step in the construction and validation of the formal object-oriented specification.     

Integral: Petri-net approach to distributed software development

As the architecture of modern software systems continues to evolve in a distributed fashion, the development of such systems becomes increasingly complex, which requires the integration of more sophisticated specification techniques, tools, and procedures into the conventional methodology. An essential capability of an integrated software development environment is a formal specification method to capture effectively the system's functional requirements as well as its performance requirements. A validation and verification (V&V) system based on a formal specification method is of paramount importance to the development and maintenance of distributed systems.

There has been recent interest in integrating software techniques and tools at the specification level. It is also noted that an effective way of achieving such integration is by using wide-spectrum specification techniques. In view of these points, an integrated V&V system, called Integral, is presented that provides comprehensive and homogeneous analysis capabilities to both specification and testing phases of the life-cycle of distributed software systems. The underlying software model that supports various V&V activities in Integral is primarily based on Petri nets and is intended to be wide spectrum. The ultimate goal of this research is to demonstrate to the software industry, domestic or foreign, the availability and applicability of a new Petri-net-based software development paradigm. Integral is a prototype V&V system to support such a paradigm.     

Telecommunications service development: A design methodology and its intelligent support

This paper describes a development life cycle for telecommunications services, emphasizing requirements capture, formal specification and validation. The service is developed along the three dimensions of the methodology: refinement, completeness and formality, aiming for a complete, consistent and formally specified service definition. The described methodology can be integrated into currently existing development life cycles which employ formal methods for service creation. Active support for the proposed life cycle is provided by a novel expert system called Requirements Assistant for Telecommunications Services (RATS), currently under development. It actively helps during requirements acquisition and early analysis, and encourages specification reuse with the help of a semi-automated negotiation process. The RATS tool advises the service developer during all stages of the service development, and on different levels of abstraction, and provides requirements management facilities, like traceability, impact analysis and document generation. Some of the features are illustrated using examples from the Universal Personal Telecommunication (UPT) service.     

基于设计演算的形式化用例分析建模框架

提出一种形式化用例分析建模框架,引入类图、用例顺序图、用例状态图、功能规约函数和系统不变式从多个角度为需求建模.通过定义这些视图的形式化语义,为需求的各个方面定义了准确的形式化描述.利用该框架,可以从方法的交互行为规约和功能规约合成描述方法全部行为的全规约;也可以定义用例模型的性质,并通过设计演算中的证明来分析验证这些性质.作为应用,研究了检查用例模型一致性的规则.给出一个实例说明建模框架的可行性.     

Systematic testing and formal verification to validate reactive programs

The use of systematic testing and formal verification in the validation of reactive systems implemented in synchronous languages is illustrated. Systematic testing and formal verification are two techniques for checking the consistency between a program and its specification. The approach to validation is through specification: two system views are developed in addition to the program, a behavioural specification for systematic testing and a logical specification for formal verification. Pursuing both activities, reactive programs can be validated both more efficiently (in terms of costs) and more effectively (in terms of confidence in correctness). This principle is demonstrated here using the well known lift example.     

Formal requirements analysis of an avionics control system

The authors report on a formal requirements analysis experiment involving an avionics control system. They describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. They critically analyze methodological issues of large scale verification and propose some practical ways of structuring verification activities for optimizing the benefits     

A requirements capture method and its use in an air traffic control application

This paper describes our experience in capturing, using a formal specification language, a model of the knowledge-intensive domain of oceanic air traffic control. This model is intended to form part of the requirements specification for a decision support system for air traffic controllers. We give an overview of the methods we used in analysing the scope of the domain, choosing an appropriate formalism, developing a domain model, and validating the model in various ways. Central to the method was the development of a formal requirements engineering environment which provided automated tools for model validation and maintenance.     

An Operational Approach to Requirements Specification for Embedded Systems

The approach to requirements specification for embedded systems described in this paper is called "operational" because a requirements specification is an executable model of the proposed system interacting with its environment. The approach is embodied by the language PAISLey, which is motivated and defined herein. Embedded systems are characterized by asynchronous parallelism, even at the requirements level; PAISLey specifications are constructed by interacting processes so that this can be represented directly. Embedded systems are also characterized by urgent performance requirements, and PAISLey offers a formal, but intuitive, treatment of performance.     

Business Processes Verification for e-Government Service Delivery

Domain experts knowledge represents a major source of information in the design and the development of user-centric and distributed service-based applications, such as those of e-government. Issues related both to the communication among domain and IT experts, and to the implementation of domain dependent requirements in service-based applications, have to be carefully considered to support both Public Administrations efficiency and citizen satisfaction. In this article, we provide as user-friendly approach toward business process assessment via formal verification. Starting from a semi-formal notation, well understood and largely used by domain experts, we provide a mapping to a formal specification in the form of a process algebra. This transformation makes possible formal and automatic verification of desired quality requirements. The approach has been already applied, with encouraging results, in the e-government domain to verify the quality of business processes related to the delivery of e-government digital services to citizens. Moreover, the approach is supported by a plug-in for the Eclipse platform permitting to have an integrated environment in which to design the process model and to assess its quality.     

Application of a Methodology for the Development and Validation of Reliable Process Control Software

This paper discusses the necessity of a good methodology for the development of reliable software, especialy with respect to the final software validation and testing activities. A formal specification development and validation methodology is proposed. This methodology has been applied to the development and validation of a pilot software, incorporating typical features of critical software for nuclear power plant safety protection. The main features of the approach indude the use of a formal specification language and the independent development of two sets of specifications. Analyses on the specifications consists of three-parts: validation against the functional requirements consistency and integrity of the specifications, and dual specification comparison based on a high-level symbolic execution technique. Dual design, implementation, and testing are performed. Automated tools to facilitate the validation and testing activities are developed to support the methodology. These includes the symbolic executor and test data generator/dual program monitor system. The experiences of applying the methodology to the pilot software are discussed, and the impact on the quality of the software is assessed.     

Formal verification of algorithms for critical systems

The authors describe their experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized     

High-level testing and example-directed development of software specifications

A testing-based approach for constructing and refining very high-level software functionality representations such as intentions, natural language assertions, and formal specifications is presented and applied to a standard line-editing problem as an illustration. The approach involves the use of specification-based (black-box) test-case generation strategies, high-level specification formalisms, redundant or parallel development and cross-validation, and a logic programming support environment. Test-case reference sets are used as software functionality representations for the purposes of cross-validating two distinct high-level representations, and identifying ambiguities and omissions in those representations. In fact, we propose the use of successive refinements of such test reference sets as the authoritative specification throughout the software development process. Potential benefits of the approach include improvements in user/ designer communication over all life cycle phases, and an increase in the quality of specifications and designs.     

Requirements specification for process-control systems

The paper describes an approach to writing requirements specifications for process-control systems, a specification language that supports this approach, and an example application of the approach and the language on an industrial aircraft collision avoidance system (TCAS II). The example specification demonstrates: the practicality of writing a formal requirements specification for a complex, process-control system; and the feasibility of building a formal model of a system using a specification language that is readable and reviewable by application experts who are not computer scientists or mathematicians. Some lessons learned in the process of this work, which are applicable both to forward and reverse engineering, are also presented     

Abstract Requirements Specification: A New Approach and Its Application

An abstract requirements specification states system requirements precisely without describing a real or a paradigm implementation. Although such specifications have important advantages, they are difficult to produce for complex systems and hence are seldom seen in the "real" programming world. This paper introduces an approach to producing abstract requirements specifications that applies to a significant class of real-world systems, including any system that must reconstruct data that have undergone a sequence of transformations. tions. It also describes how the approach was used to produce a requirements document for SCP, a small, but nontrivial Navy communications system. The specification techniques used in the SCP requirements document are introduced and illustrated with examples.     

A service creation environment based on scenarios

Scenarios are often constructed for illustrating example runs through reactive system. Scenarios that describe possible interactions between a system and its environment are widely used in requirement engineering, as a means for users to communicate their functional requirements. Various software development methods use scenarios to define user requirements, but often lack tool support. Existing tools are graphical editors rather than tool support for design. This paper presents a service creation environment for elicitation, integration, verification and validation of scenarios. A semi-formal language is defined for user oriented scenario representation, and a prototype tool implementing an algorithm that integrates them for formal specification generation. This specification is then used to automatically find and report inconsistencies in the scenarios.     

Requirements engineering: the state of the practice

Little contemporary data exists for document actual practices of software professionals for software requirements elicitation, requirements specification, document development, and specification validation. This exploratory survey and its quantitative results offer opportunities for further interpretation and comparison.     

结合形式化的面向对象设计方法与支撑系统

为了有效地结合形式化和非形式化设计方法各自的优点,克服其不足之处,以尽可能保证软件设计的质量与可靠性,文章提出了一种将形式化方法与非形式化的面向对象设计方法ＨＯＯＤ（ｈｉｅｒａｒｃｈｉｃａｌｏｂｊｅｃｔ－ｏｒｉｅｎｔｅｄｄｅｓｉｇｎ）相结合的途径,并介绍了其机器支撑环境的设计与实现．该途径在对层次式面向对象设计方法ＨＯＯＤ进行必要扩充的基础上,有机地集成了Ｚ语言等形式规约技术．支持这一途径的支撑环境提供了一套方便灵活的图形构筑工具、语法制导的形式语言与文本编辑工具,以及自动检查机制等．