Optimal parallel verification of minimum spanning trees in logarithmic time

We present the first optimal parallel algorithms for the verification and sensitivity analysis of minimum spanning trees. Our algorithms are deterministic and run inO(logn) time and require linear-work in the CREW PRAM model. These algorithms are used as a subroutine in the linear-work randomized algorithm for finding minimum spanning trees of Cole, Klein, and Tarjan. Research partially supported by a National Science Foundation Graduate Fellowship and by DIMACS (Center for Discrete Mathematics and Theoretical Computer Science), a National Science Foundation Science and Technology Center, Grant No. NSF-STC88-09648. Research at Princeton University was partially supported by the National Science Foundation, Grant No. CCR-8920505, the Office of Naval Research, Contract No. N00014-91-J-1463, and by DIMACS (Center for Discrete Mathematics and Theoretical Computer Science), a National Science Foundation Science and Technology Center, Grant No. NSF-STC88-09648.     

A survey of tools for the validation and verification of knowledge-based systems: 1985-1995

This paper presents the findings of a survey of software tools built to assist in the verification and validation of knowledge-based systems. The tools were identified from literature sources from the period 1985-1995. The tool builders were contacted and asked to complete and return a survey that identified which testing and analysis techniques were utilised and covered by their tool. From these survey results it is possible to identify trends in tool development, technique coverage and areas for future research.     

Verification of a sliding window protocol in μCRL and PVS

We prove the correctness of a sliding window protocol with an arbitrary finite window size n and sequence numbers modulo 2n. The correctness consists of showing that the sliding window protocol is branching bisimilar to a queue of capacity 2n. The proof is given entirely on the basis of an axiomatic theory, and has been checked in the theorem prover PVS. Received November 2004 Revised June 2005 Accepted July 2005 by J. V. Tucker     

State-space caching revisited

State-space caching is a verification technique for finite-state concurrent systems. It performs an exhaustive exploration of the state space of the system being checked while storing only all states of just one execution sequence plus as many other previously visited states as available memory allows. So far, this technique has been of little practical significance: it allows one to reduce memory usage by only twoo to three times, before an unacceptable blow-up of the run-time overhead sets in. The explosion of the run-time requirements is due to redundant multiple explorations of unstored parts of the state space. Indeed, almost all states in the state space of concurrent systems are typically reached several times during the search.In this paper, we present a method to tackle the main cause of this prohibitive state matching: the exploration of all possible interleavings of concurrent executions of the system which all lead to the same state. Then, we show that, in many cases, with this method, most reachable states are visited only once during state-space exploration. This enables one not to store most of the states that have already been visited without incurring too much redundant explorations of parts of the state space, and makes therefore state-space caching a much more attractive verification method. As an example, we were able to competely explore a state space of 250,000 states while storing simultaneously no more than 500 states and with only a three-fold increas of the run-time requirements.     

A numerical study on low and higher-order potential based BEM for 2D inviscid flows

A formal error analysis of the order of approximation of a potential based boundary element method (BEM) for two-dimensional flows is performed in order to derive consistent approximations for the potential integrals. Two higher-order approaches satisfying consistency requirements to attain second and third order convergence in the potential are selected for numerical implementation. From the formal local expansions of the potential integrals the influence coefficients are derived and evaluated analytically. In order to assess the methods accuracy, the low and higher-order methods are applied to two-dimensional steady flows around analytical foils. A numerical error analysis is done and a comparison between their theoretical and numerical asymptotic order of accuracy performed. The first author acknowledges the financial support granted by Fundação para a Ciência e a Tecnologia, Ph.D. grant PRAXISXXI/BD/2226/99. This work was done under the project PRAXIS/2/2.1/MAR/1723/95.     

Verification and validation of an intelligent tutorial system

This paper presents the results of a verification and validation process for an intelligent system. The system being studied is an Intelligent Tutorial that employs fuzzy logic and multiagent systems. Software engineering techniques were used in the verification process, while the validation exploited both qualitative and quantitative techniques.     

数字仿真模型的校核验证和测试 (一)

介绍数字仿真模型的校核、验证和测试的基本概念，并提出了些实际的实行方法。     

进口经纬仪检定中亟待解决的问题

总结了作者几年来从事进口经纬仪检定工作的部分体会，就存在的几个问题进行了讨论。     

STG-BASED VERIFICATION AND TEST GENERATION

This paper presents the techniques of verification and Test Generation(TG) for sequential machines (Finite State Machines, FSMs) based on state traversing of State Transition Graph(STG). The problems of traversing, redundancy and transition fault model are identified. In order to achieve high fault coverage collapsing testing is proposed. Further, the heuristic knowledge for speeding up verification and TG are described.     

221厂核设施退役工程的竣工验收辐射检测

本文叙述２２１厂核设施退役工程的竣工验收辐射检测，内容涉及竣工验收辐射检测小组的职能和组织形式，验收检测标准，验收检测的实施及其主要结果。