Proving the Correctness of the Standardized Algorithm for ABR Conformance

Conformance control for ATM cells is based on a real-time reactive algorithm which delivers a value depending on inputs from the network. This value must always fit with a well defined theoretical value. We present here the correctness proof of the algorithm standardized for the ATM transfer capability called ABR. The proof turned out to produce a key argument during the standardization process of ABR.     

Verifying Temporal Properties of Reactive Systems: A STeP Tutorial

We review a number of formal verification techniques supported by STeP, the Stanford Temporal Prover, describing how the tool can be used to verify properties of several versions of the Bakery Mutual exclusion algorithm for mutual exclusion. We verify the classic two-process algorithm and simple variants, as well as an atomic parameterized version. The methods used include deductive verification rules, verification diagrams, automatic invariant generation, and finite-state model checking and abstraction.     

NC图形验证与仿真技术的研究概况

数控程序图形验证与仿真技术的研究对保证加工质量提高加工效率具有重要意义,同时也是虚拟制造技术的主要研究内容之一,该文从国外NC几何验证、NC物理验证以及我国的NC图形验证三个方面对NC图形验证技术的发展概况作了较全面的论述,并指出其中存在的不足和尚待解决的问题。最后提出一种新的复杂曲面NC图形验证的体系结构。     

A framework for computer-aided validation

This paper presents a framework for augmenting independent validation and verification (IV&V) of software systems with computer-based IV&V techniques. The framework allows an IV&V team to capture its own understanding of the application as well as the expected behavior of any proposed system for solving the underlying problem by using an executable system reference model, which uses formal assertions to specify mission- and safety-critical behaviors. The framework uses execution-based model checking to validate the correctness of the assertions and to verify the correctness and adequacy of the system under test.     

A Comparison of Free BDDs and Transformed BDDs

Ordered binary decision diagrams (OBDDs) introduced by Bryant (IEEE Trans. on Computers, Vol. 35, pp. 677–691, 1986) have found a lot of applications in verification and CAD. Their use is limited if the OBDD size of the considered functions is too large. Therefore, a variety of generalized BDD models has been presented, among them FBDDs (free BDDs) and TBDDs (transformed BDDs). Here the quite tight relations between these models are revealed and their advantages and disadvantages are discussed.     

Bounded Model Checking Using Satisfiability Solving

The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.     

Automatic Real-Time Analysis of Reactive Systems with the PARTS Toolset

Real-time systems are becoming increasingly widespread, often in safety-critical applications. It is therefore crucial that these systems be correct; however, there are few automated tools for analyzing concurrency and timing properties of these systems. The PARTS toolset uses a Petri-net-based reachability analysis to analyze program specifications written in an Ada-83 subset. Our simple time Petri nets are specifically aimed at facilitating real-time analysis. In order to control the state-explosion problem, PARTS employs several optimization techniques aimed at state-space reduction. In this paper we discuss our approach and we report on extensive experiments with several examples of real-time specifications based on Ada 83. When possible, we also compare our experimental results with results obtained by other approaches to real-time analysis.     

Gaining Confidence in Software Inspection Using a Bayesian Belief Model

In this paper I describe how confidence in a software inspection can be obtained through calculating an estimate of its effectiveness. The method uses a Bayesian Belief Network to model the software inspection process and calculates the inference on how effective a particular inspection was. This technique was selected as it provides a means of initialising the model with inspectors' experience and has the ability to learn and optimise performance. This technique provides answers to some of the questions and limitations raised by current models used to predict inspection effectiveness. The application of the model to a major software project is discussed, covering the initial practitioner survey, model initialisation, model calibration and verification results obtained.     

An Algorithm for Timing Verification of Systems Constrained by Min–max Inequalities

To determine the maximum separation between events for nonrepetitive systems with max and linear constraints, there are the “iterative tightening from above” (ITA) approach and the “iterative tightening from below” (ITB) approach. Since such systems can be formulated as systems constrained by min–max inequalities, this paper gives an algorithm named MMIMaxSep for solving min–max inequalities. The algorithm is a generalization and a mathematically elegant reformulation of Yen et al.’s MaxSeparation algorithm which uses the ITB approach. Our numerical experiments indicate that MMIMaxSep is very efficient. Moreover, MMIMaxSep has a unique advantage of being able to directly handle tree-represented min–max functions, and its complexity is closely related to the complexity of computing cycle time of min–max functions.