Control and data abstraction: the cornerstones of practical formal verification

In spite of the impressive progress in the development of the two main methods for formal verification of reactive systems – Symbolic Model Checking and Deductive Verification, they are still limited in their ability to handle large systems. It is generally recognized that the only way these methods can ever scale up is by the extensive use of abstraction and modularization, which break the task of verifying a large system into several smaller tasks of verifying simpler systems. In this paper, we review the two main tools of compositionality and abstraction in the framework of linear temporal logic. We illustrate the application of these two methods for the reduction of an infinite-state system into a finite-state system that can then be verified using model checking. The technical contributions contained in this paper are a full formulation of abstraction when applied to a system with both weak and strong fairness requirements and to a general temporal formula, and a presentation of a compositional framework for shared variables and its application for forming network invariants.     

An approach to formal verification of human–computer interaction

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.     

Improving the security of industrial networks by means of formal verification

Computer networks are exposed to serious security threats that can even have catastrophic consequences from both the points of view of economy and safety if such networks control critical infrastructures, such as for example industrial plants. Security must then be considered as a fundamental issue starting from the earlier phases of the design of a system, and suitable techniques and tools should be adopted to satisfy the security-related requirements. The focus of this paper is on how formal methods can help in analysing the standard cryptographic protocols used to implement security-critical services such as authentication and secret keys distribution in critical environments. The analysis of the 802.11 shared key authentication protocol by S³A, a fully automatic software tool that is based on a formal approach, is illustrated as a case study, which also highlights the peculiarities of analysing protocols based on wireless channels.     

Formal verification of behaviour networks including sensor failures

The paper deals with the problem of verifying behaviour-based control systems. Although failures in sensor hardware and software can have strong influences on the robot’s operation, they are often neglected in the verification process. Instead, perfect sensing is assumed. Therefore, this paper provides an approach for modelling the sensor chain in a formal way and connecting it to the formal model of the control system. The resulting model can be verified using model checking techniques, which is shown on the examples of the control systems of an autonomous indoor robot and an autonomous off-road robot.     

Applying abstraction and formal specification in numerical software design

Numerical software development tends to struggle with an increasing complexity. This is, on the one hand, due to the integration of numerical models, and on the other hand, due to change of hardware. Parallel computers seem to fulfill the need for more and more computer resources, but they are more complex to program.

The article shows how abstraction is used to combat complexity. It motivates that separating a specification, “what,” its realisation, “how,” and its implementation, “when, where,” is of vital importance in software development. The main point is that development steps and levels of abstraction are identified, such that the obtained software has a clear and natural structure.

Development steps can be cast into a formal, i.e., mathematical framework, which leads to rigourous software development. This way of development leads to accurate and unambiguous recording of development steps, which simplifies maintenance, extension and porting of software. Portability is especially important in the field of parallel computing where no universal parallel computer model exists.     

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.     

通信网络在智能建筑中的应用研究

对智能建筑通信网络(IBN)进行了研究，重点分析了：智能建筑信息系统(IBIS)网络的集成以及将不同的建筑系统集成于一个框架内的标准协议的应用．而ISDN与ADSL被认为是实现IBN的合适平台。     

On the interaction between localization and location verification for wireless sensor networks

Secure wireless sensor networks (WSNs) must be able to associate a set of reported data with a valid location. Many algorithms exist for the localization service that determines a WSN node’s location, and current research is developing for location verification, where the network must determine whether or not a node’s claimed location is valid (or invalid). However, the interaction of these two services creates another challenge, since there is no method to distinguish between benign errors, e.g., errors that are inherent to the localization technique, and malicious errors, e.g., errors due to a node’s deceptive location report. In this paper, we study the problem of inherent localization errors and their impact on the location verification service. We propose a localization and location verification (LLV) server model, and define categories of LLV schemes for discrete and continuous resolution. We then designate two metrics to measure the impact of inherent localization errors—the probability of verification (for the discrete location verification schemes) and the CDF of the deviation distance (for the continuous location verification schemes)—to analyze the performance of each LLV category. Numerical results show that a proper tuning mechanism is needed to tolerate even small inherited estimation errors, otherwise the location verification can result in the rejection of almost all nodes. In addition, we propose several location verification feedback (LV-FEED) algorithms to improve the localization accuracy. Analysis of these algorithms shows that a significant improvement in localization accuracy can be accomplished in a few iterations of executing the location verification feedback schemes.     

An approach to formal specification and verification of map-centered applications

Users in the domain of map-centered applications who want to specify a new application rely only on informal languages such as English. There is also no standardized terminology, resulting in ambiguous specifications. This work proposes an approach to specify and verify map-centered applications. This domain has been studied under different perspectives but there is a lack of research from the software engineering viewpoint. We characterize the domain by presenting a classification of different space models that appear in the Geographical Information Systems (GIS) literature, as well as of some of the problems addressed by map-centered applications. The proposed solution includes a language with semantics based in a formalization of each space model. This helps in verifying properties over a specification written using the formal language.     

Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes

The design of complex inter-enterprise business processes (IEBP) is generally performed in a modular way. Each process is designed separately and then the whole IEBP is obtained by composition. Even if such a modular approach is intuitive and facilitates the design problem, it poses the problem that correct behavior of each business process of the IEBP taken alone does not guarantee a correct behavior of the composed IEBP (i.e. properties are not preserved by composition). Proving correctness of the (unknown) composed process is strongly related to the model checking problem of a system model. Among others, the symbolic observation graph based approach has proven to be very helpful for efficient model checking in general. Since it is heavily based on abstraction techniques and thus hides detailed information about system components that are not relevant for the correctness decision, it is promising to transfer this concept to the problem raised in this paper: How can the symbolic observation graph technique be adapted and employed for process composition? Answering this question is the aim of this paper.     

Application of BDDs in Boolean matching techniques for formal logic combinational verification

Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods. Published online: 15 May 2001     

The service system is the basic abstraction of service science

Abstraction is a powerful thing. During the nineteenth century, the Industrial Revolution was built on many powerful abstractions, such as mass, energy, work, and power. During the twentieth century, the information revolution was built on many powerful abstractions, such as binary digit or bit, binary coding, and algorithmic complexity. Here, we propose an abstraction for the twenty-first century, in which there is an emerging revolution in thinking about business and economics based on a service-dominant logic. The worldview of service-dominant logic stands in sharp contrast to the worldview of the goods-dominant logic of the past, as it holds service—the application of competences for benefit of others—rather than goods to be the fundamental basis of economic exchange. Within this new worldview, we suggest the basic abstraction is the service system, a configuration of people, technologies, and other resources that interact with other service systems to create mutual value. Many systems can be viewed as service systems, including families, cities, and companies, among many others. In this paper, we show how the service-system abstraction can be used to understand how value is co-created, in the process laying the foundation for an integrated science of service.

Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

The problem of verification with reference to the Girkmann problem

This paper is concerned with the problem of verification of the numerical accuracy of computed information with particular reference to a model problem in solid mechanics. The basic concepts and procedures are outlined and illustrated by examples.     

Specification and verification of object-oriented programs using supertype abstraction

We present a formal specification language and a formal verification logic for a simple object-oriented programming language. The language is applicative and statically typed, and supports subtyping and message-passing. The verification logic relies on a behavioral notion of subtyping that captures the intuition that a subtype behaves like its supertypes. We give a formal definition for legal subtype relations, based on the specified behavior of objects, and show that this definition is sufficient to ensure the soundness of the verification logic. The verification logic reflects the way programmers reason informally about object-oriented programs, in that it allows them to use static type information, which avoids the need to consider all possible run-time subtypes.The work of both authors was supported in part by the National Science Foundation under Grant CCR-8716884, and in part by the Defense Advanced Research Projects Agency (DARPA) under Contract N00014-89-J-1988. While a graduate student at MIT, Leavens was also supported in part by a GenRad/AEA Faculty Development Fellowship, and at ISU he has been partially supported by the ISU Achievement Foundation and by the National Science Foundation under Grant CCR-9108654     

The feature and service interaction problem in telecommunicationssystems: a survey

Today's telecommunication systems are enhanced by a large and steadily growing number of supplementary services, each of which consists of a set of service features. A situation where a combination of these services behaves differently than expected from the single services' behaviors, is called service interaction. This interaction problem is considered as a major obstacle to the introduction of new services into telecommunications networks. We present a survey of the work carried out in this field during the last decade (1988-98). After a brief review of classification criteria that exist for feature interactions so far, we use a perspective called the emergence level view. This perspective pays respect to the fact that the sources for interactions can be of many different kinds, e.g., requirement conflicts or resource contentions. It is used to rationalize the impossibility of coping with the problem with one single approach. We also present a framework of four different criteria in order to classify the approaches dealing with the problem. The general kind of approach taken, a refinement of the well known detection, resolution, and prevention categories, serves as the main classification criterion. It is complemented by the method used, the stage during the feature lifecycle where an approach applies, and the system (network) context. The major results of the different approaches are then presented briefly using this classification framework. We finally draw some conclusions on the applicability of this framework and on possible directions of further research in this field     

Object-oriented specification and formal verification of real-time systems

An object-oriented approach for specification and verification of real-time systems is described in this paper. It is motivated by taking advantage of object-oriented techniques to produce real-time software that is easy to understand, maintain, and reuse. The approach specifies the structural, behavioral, and control aspects of objects in one model with a textual representation as well as a graphical representation. For ease to comprehend and use, the model encapsulates object states and allows an analyst to focus on specifying object operations one at a time. System behavior from individual objects can be deduced and analyzed. For safety considerations, the approach supports specification of failures to object behavior and their resultant faults. The approach also supports modeling of timed temporal constraints for specifying and verifying desirable real-time properties. An object timed temporal logic OTTL is defined for expressing the syntax and semantics of these constraints. Decision procedures for their verification are also presented.