White-box testing allows developers to determine whether or not a program is partially consistent with its specified behavior and design through the examination of intermediate values of variables during program execution. These intermediate values are often recorded as an execution trace produced by monitoring code inserted into the program. After program execution, the values in an execution trace are compared to values predicted by the specified behavior and design. Inconsistencies between predicted and actual values can lead to the discovery of errors in the specification and its implementation. This paper describes an approach to (1) verify the execution traces created by monitoring statements during white-box testing using a model checker as a semantic tableau; (2) organize multiple execution traces into distinct equivalence partitions based on requirements specifications written in linear temporal logic (LTL); and (3) use the counter-example generation mechanisms found in most model-checker tools to generate new test cases for unpopulated equivalence partitions.

This paper describes the process of implementing a complex communications protocol that provides reliable delivery of data in multicast-capable, packet-switching telecommunication networks. The protocol, called the Reliable Multicasting Protocol (RMP), was developed incrementally using a combination of formal and informal techniques in an attempt to ensure the correctness of its implementation. Our development process involved three concurrent activities: (1) the initial construction and incremental enhancement of a formal state model of the protocol machine; (2) the initial coding and incremental enhancement of the implementation; and (3) model-based testing of iterative implementations of the protocol. These activities were carried out by two separate teams: a design team and a V&V team. The design team built the first version of RMP with limited functionality to handle only nominal requirements of data delivery. This initial version did not handle off-nominal cases such as network partitions or site failures. Meanwhile, the V&V team concurrently developed a formal model of the requirements using a variant of SCR-based state tables. Based on these requirements tables, the V&V team developed test cases to exercise the implementation. In a series of iterative steps, the design team added new functionality to the implementation while the V&V team kept the state model in fidelity with the implementation. This was done by generating test cases based on suspected errant or off-nominal behaviors predicted by the current model. If the execution of a test in the model and implementation agreed, then the test either found a potential problem or verified a required behavior. However, if the execution of a test was different in the model and implementation, then the differences helped identify inconsistencies between the model and implementation. In either case, the dialogue between both teams drove the co-evolution of the model and implementation. We have found that this interactive, iterative approach to development allows software designers to focus on delivery of nominal functionality while the V&V team can focus on analysis of off-nominal cases. Testing serves as the vehicle for keeping the model and implementation in fidelity with each other. This paper describes (1) our experiences in developing our process model; and (2) three example problems found during the development of RMP. Although RMP has provided our research effort with a rich set of test cases, it also has practical applications within NASA. For example, RMP is being considered for use in the NASA EOSDIS project due to its significant performance benefits in applications that need to replicate large amounts of data to many network sites. The RMP source code and documentation are currently available on the WWW via

We present the Wireless Routing Protocol (WRP). In WRP, routing nodes communicate the distance and second-to-last hop for each destination. WRP reduces the number of cases in which a temporary routing loop can occur, which accounts for its fast convergence properties. A detailed proof of correctness is presented and its performance is compared by simulation with the performance of the distributed Bellman-Ford Algorithm (DBF), DUAL (a loop-free distance-vector algorithm) and an Ideal Link-state Algorithm (ILS), which represent the state of the art of internet routing. The simulation results indicate that WRP is the most efficient of the alternatives analyzed.

We propose a combination of model checking and interactive theorem proving where the theorem prover is used to represent finite and infinite state systems, reason about them compositionally and reduce them to small finite systems by verified abstractions. As an example we verify a version of the Alternating Bit Protocol with unbounded lossy and duplicating channels: the channels are abstracted by interactive proof and the resulting finite state system is model checked.

PVS is an automated tool for specification and verification that is designed to exploit the synergies between language and deduction, automation and interaction, and theorem proving and model checking. PVS strives for a balance between automation and interaction by using decision procedures to simplify the tedious and obvious steps in a proof leaving the user to interactively supply the high-level steps in a verification. Decision procedures for BDD-based propositional simplification and model checking, equality, and linear arithmetic are integrated into PVS. The utility of the language and deductive features of PVS have been demonstrated in a number of examples, including the specification and partial verification of the Rockwell-Collins AAMP5 processor design, and the verification of an SRT divider. This tutorial concentrates on the integration of individual verification techniques available in PVS.

We survey recent progress in the development of mathematical techniques for specifying and verifying complex hardware and software systems. Many of these techniques are capable of handling industrial-sized examples; in fact, in some cases these techniques are already being used on a regular basis in industry. Success in formal specification can be attributed to notations that are accessible to system designers and to new methodologies for applying these notations effectively. Success in verification can be attributed to the development of new tools such as more powerful theorem provers and model checkers than were previously available. Finally, we suggest some general research directions that we believe are likely to lead to technological advances. Although it is difficult to predict where the future advances will come, optimism about the next generation of formal methods is justified in view of the progress during the past decade. Such progress, however, will strongly depend on continued support for basic research on new specification languages and new verification techniques.

The testing process is typically systematic in test data selection and test execution. For the most part, however, the effective use of test oracles has been neglected, even though they are a critical component of the testing process. Test oracles prescribe acceptable behavior for test execution. In the absence of judging test results with oracles, testing does not achieve its goal of revealing failures or assuring correct behavior in a practical manner; manual result checking is neither reliable nor cost-effective. <p> We argue that test oracles should be derived from specifications and in conjunction with testing criteria, represented in a common form, and their use made integral to the testing process. For complex, reactive systems, oracles must reflect the multiparadigm nature of the required behavior. Such systems are often specified using multiple languages, each selected for its utility in specifying a particular computational paradigm. Thus, we are developing an approach for deriving and using oracles based on multiparadigm and multilingual specifications to enable the verification of test results for reactive systems as well as less complex systems.

This paper describes a generic tableau algorithm, which is the basis for a general customizable method for producing oracles from temporal logic specifications. A generic argument gives semantic rules with which to build the semantic tableau for a specification. Parameterizing the tableau algorithm by semantic rules permits it to easily accommodate a variety of temporal operators and provides a clean mechanism for fine-tuning the algorithm to produce efficient oracles. <p> The paper develops conditions to ensure that a set of rules results in a correct tableau procedure. It gives sample rules for a variety of linear-time temporal operators and shows how rules are tailored to reduce the size of an oracle.

Effective testing of critical systems has been hampered by the lack of a cost-effective method for deciding the correctness of a program's behavior under test. Using formal specifications to describe the critical system properties and then checking test results against these specifications overcomes these problems. If these <i> test oracles</i>, which are mechanisms for determining whether a test passes or fails, are efficient, they can be combined with automatic test generation to cost-effectively automate the testing of large numbers of testcases that more adequately cover the system requirements and structure. This paper presents a algorithm for automatically deriving efficient test oracles from Graphical Interval Logic (GIL), which is a graphical temporal logic that is easier for non-experts to understand than many formal languages. To develop efficient test oracles from GIL, we convert the specifications into automata that can be checked in time linear in the length of the trace. Additionally, the automata can be checked incrementally to identify the failure when it occurs, which provides the opportunity to obtain useful information about the erroneous state of the system. We have implemented a tool that converts GIL specifications into automata based on the algorithms presented in this paper.

Few would question that software testing is a necessary activity for assuring software quality, yet the typical testing process is a human intensive activity and as such, it is unproductive, error-prone, and often inadequately done. Moreover, testing is seldom given a prominent place in software development or maintenance processes, nor is it an integral part of them. Major productivity and quality enhancements can be achieved by automating the testing process through tool development and use and effectively incorporating it with development and maintenance processes. <p> The TAOS toolkit, Testing with Analysis and Oracle Support, provides support for the testing process. It includes tools that automate many tasks in the testing process, including management and persistence of test artifacts and the relationships between those artifacts, test development, test execution, and test measurement. A unique aspect of TAOS is its support for test oracles and their use to verify behavioral correctness of test executions. TAOS also supports structural/dependence coverage by measuring the adequacy of test criteria coverage and regression testing by identifying tests associated or dependent upon modified software artifacts. This is accomplished by integrating the ProDAG toolset, Program Dependence Analysis Graph, with TAOS. The combination of ProDAG and TAOS supports the use of program dependence analysis in testing, debugging, and maintenance. <p> This paper describes the TAOS toolkit and its capabilities as well as testing, debugging and maintenance processes based on program dependence analysis. We also describe our experience with the toolkit and discuss our future plans.

Testing commercial software is expensive and time consuming. Automated testing methods promise to save a great deal of time and money throughout the software industry. One approach that is well-suited for the reactive systems found in telephone switching systems is specification-based testing.

We have built a set of tools to automatically test software applications for violations of safety properties expressed in temporal logic. Our testing system automatically constructs finite state machine oracles corresponding to safety properties, builds test harnesses, and integrates them with an application. The test harness then generates inputs automatically to test the application. We describe a study examining the feasibility of this approach for testing industrial applications. To conduct this study we formally modeled an Automatic Protection Switching system (APS), which is an application common to many telephony systems. We then asked a number of computer science graduate students to develop several versions of the APS and use our tools to test them. We found that the tools are very effective, save significant amounts of human effort (at the expense of machine resources), and are easy to use. We also discuss improvements that are needed before we can use the tools with professional developers building commercial products.

Verifying that test executions are correct is a crucial step in the testing process. Unfortunately, it can be a very arduous and error-prone step, especially when testing a concurrent system. System developers can therefore benefit from oracles automating the verification of test executions.<p> This paper examines the use of Graphical Interval Logic (GIL) for specifying temporal properties of concurrent systems and describes a method for constructing oracles from GIL specifications. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than specifications written in more traditional temporal logics. Additionally, when a test execution violates a GIL specification, the associated oracle provides information about a fault. This information can be displayed visually, together with the execution, to help the system developer see where in the execution a fault was detected and the nature of the fault.<p>

Formal description techniques (FDT's) are useful in the protocol development cycle, particulary in the conformance testing area. In this paper, we present TETRA, a test and trace analysis tool based on the LOTOS FDT which can be used to automatically compare the specified verdicts of a conformance test case with a protocol specification, or to analyse results of a test run with the reference specification. We also describe our experience with this tool for the validation of a X.25 TTCN test suite and for the testing of an ACSE implementation.

There are two aspects to testing: (1) the selection of appropriate test inputs and (2) the analysis of the observed interactions of the implementation under test (IUT) in order to determine whether they conform to the IUT's specification. The paper considers the second aspect with particular attention to the testing of OSI communication protocol implementations. A system is described which analyses an observed test trace of interactions with respect to a reference specification which is assumed to be written in LOTOS. In the case that an error is detected, the system also provides some diagnostic information for locating the &quot;error&quot; in the analyzed trace. The practical use of such a trace analysis system is discussed, as well as the possibility of using a similar approach for the validation of the verdicts which are included in the standardized OSI conformance test cases.

This paper describes a modest conservative extension of HOL90 that allows the results from external decision procedures to be used within HOL90 without compromising its logical consistency.

This paper describes MTSim, an extensible, customizable simulation platform for the Modechart Toolset (MT). MTSim provides support for ``plugging in'' of user-defined viewers which display simulation behavior in different ways including application-specific displays. In addition, MTSim supports full user participation in the generation of simulations through the injection of events into the execution trace. Moreover, MTSim supports monitoring and assertion-checking of execution traces, invoking user-specified handlers upon assertion violation. This paper also introduces WebSim, a web-centric suite of simulation tools for MT, on top of the MTSim platform. It also describes a application-specific interface built on MTSim which represents the cockpit of an F-18 aircraft and models its bomb-release

A formalism is presented for specification and analysis of real-time constraints of systems at run time. Real-time logic (RTL) is employed to illustrate how timing properties can be specified elegantly in the form of annotation added to a program (or to a design specification). The algorithms for detecting a violation of a timing property at runtime, expressed in RTL, are presented.