The 1976 paper describes the early development of a Symbolic Execution systems including some of the software engineering challenges, before internet communication and interactive computing were the norm. It describes the early expectations for such systems and contrasts those with the actual benefits and difficulties that arose. It also describes some of the surprising lessons learned.

In this article, we present an approach for systematically improving complex processes, especially those involving human agents, hardware devices, and software systems. We illustrate the utility of this approach by applying it to part of an election process and show how it can improve the security and correctness of that subprocess. We use the Little-JIL process definition language to create a precise and detailed definition of the process. Given this process definition, we use two forms of automated analysis to explore whether specified key properties, such as security and safety policies, can be undermined. First, we use model checking to identify process execution sequences that fail to conform to event-sequence properties. After these are addressed, we apply fault tree analysis to identify when the misperformance of steps might allow undesirable outcomes, such as security breaches. The results of these analyses can provide assurance about the process; suggest areas for improvement; and, when applied to a modified process definition, evaluate proposed changes.

Summary form only given. As has been widely reported in the news lately, healthcare errors are a major cause of death and suffering. In the University of Massachusetts Medical Safety Project, we are exploring the use of process modeling and analysis technologies to help reduce medical errors and improve efficiency. Specifically, we are modeling healthcare processes using a process definition language and then analyzing these processes using model checking, fault-tree analysis, discrete event simulation, and other techniques. Working with the UMASS School of Nursing and the Baystate Medical Center, we are undertaking in-depth case studies on error-prone and life-critical healthcare processes. In many ways, these processes are similar to complex, distributed systems with many interacting, concurrent threads and numerous exceptional conditions that must be handled carefully. This talk describes the technologies we are using, discusses case studies, and presents our observations and findings to date. Although presented in terms of the healthcare domain, the described approach could be applied to human-intensive processes in other domains to provide a technology-driven approach to process improvement.

Society faces increasing reliance on software-intensive systems to manage health services, from scheduling, billing, and patient records to the control of life-critical devices and procedures. There are important concerns about software quality, security, and privacy, user interfaces, system interoperability, process automation and improvement, and many other issues of current concern to software engineering practitioners and researchers. It is widely recognized that information and communication technologies (ICTs) will transform healthcare of the future, being a driving force for improving care and access, while reducing the overall cost when broadly calculated based on overall productivity and quality of life.

With the availability of powerful computational and communication systems, scientists now readily access large, complicated derived datasets and build on those results to produce, through further processing, yet other derived datasets of interest. The scientific processes used to create such datasets must be clearly documented so that scientists can evaluate their soundness, reproduce the results, and build upon them in responsible and appropriate ways. Here, we present the concept of ananalytic web, which defines the scientific processes employed and details the exact application of those processes in creating derived datasets. The work described here is similar to work often referred to as “scientific workflow,” but emphasizes the need for a semantically rich, rigorously defined process definition language. We illustrate the information that comprises an analytic web for a scientific process that measures and analyzes the flux of water through a forested watershed. This is a complex and demanding scientific process that illustrates the benefits of using a semantically rich, executable language for defining processes and for supporting automatic creation of process provenance metadata.

This paper shows how software engineering technologies used to define and analyze complex software systems can also be effective in detecting defects in human-intensive processes used to administer healthcare. The work described here builds upon earlier work demonstrating that healthcare processes can be defined precisely. This paper describes how finite-state verification can be used to help find defects in such processes as well as find errors in the process definitions and property specifications. The paper includes a detailed example, based upon a real-world process for transfusing blood, where the process defects that were found led to improvements in the process.

This paper describes our experiences in exploring the applicability of software engineering approaches to scientific data management problems. Specifically, this paper describes how process definition languages can be used to expedite production of scientific datasets as well as to generate documentation of their provenance. Our approach uses a process definition language that incorporates powerful semantics to encode scientific processes in the form of a Process Definition Graph (PDG). The paper describes how execution of the PDG-defined process can generate Dataset Derivation Graphs (DDGs), metadata that document how the scientific process developed each of its product datasets. The paper uses an example to show that scientific processes may be complex and to illustrate why some of the more powerful semantic features of the process definition language are useful in supporting clarity and conciseness in representing such processes. This work is similar in goals to work generally referred to as Scientific Workflow. The paper demonstrates the contribution that software engineering can make to this domain.

Finite-state verification techniques are often hampered by the state-explosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning, where a system under analysis is partitioned into subsystems and these subsystems are analyzed individually. By composing the results of these analyses, it can be determined whether or not the system satisfies a property. Because each subsystem is smaller than the whole system, analyzing each subsystem individually may reduce the overall cost of verification. Often the behavior of a subsystem is dependent on the subsystems with which it interacts, and thus it is usually necessary to provide assumptions about the environment in which a subsystem executes. Because developing assumptions has been a difficult manual task, the evaluation of assume-guarantee reasoning has been limited. Using recent advances for automatically generating assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks in these systems, we evaluated the decompositions as they were scaled. We found that in only a few cases can assume-guarantee reasoning verify properties on larger systems than monolithic verification can, and in these cases the systems that can be analyzed are only a few sizes larger. Although these results are discouraging, they provide insight about research directions that should be pursued and highlight the importance of experimental evaluation in this area.

We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. This method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic execution, to establish the equivalence of the two programs. In this approach the path condition from symbolic execution of the sequential program is used to constrain the search through the parallel program. To handle floating-point operations, three different types of equivalence are supported. Several examples are presented, demonstrating the approach and actual errors that were found. Limitations and directions for future research are also described.

Finite-state verification (FSV) techniques attempt to prove properties about a model of a system by examining all possible behaviors of that model. This approach suffers from the state-explosion problem, where the size of the model or the analysis costs may be exponentially large with respect to the size of the system. Using symbolic data structures to represent subsets of the state space has been shown to usually be an effective optimization approach for hardware verification. The value for software verification, however, is still unclear. In this paper, we investigate applying two symbolic data structures, Binary Decision Diagrams (BDDs) and Zero-suppressed Binary Decision Diagrams (ZDDs), in two FSV tools, LTSA and FLAVERS. We describe an experiment showing that these two symbolic approaches can improve the performance of both FSV tools and are more efficient than two other algorithms that store the state space explicitly. Moreover, the ZDD-based approach often runs faster and can handle larger systems than the BDD-based approach.

Finite-state verification techniques are often hampered by the stateexplosion problem. One proposed approach for addressing this problem is assume-guarantee reasoning. Using recent advances in assume-guarantee reasoning that automatically generate assumptions, we undertook a study to determine if assume-guarantee reasoning provides an advantage over monolithic verification. In this study, we considered all two-way decompositions for a set of systems and properties, using two different verifiers, FLAVERS and LTSA. By increasing the number of repeated tasks, we evaluated the decompositions as the systems were scaled. In only a few cases could assume-guarantee reasoning verify properties on larger systems than monolithic verification and, in these cases, assumeguarantee reasoning could only verify these properties on systems a few sizes larger than monolithic verification. This discouraging result, although preliminary, raises doubts about the usefulness of assume-guarantee reasoning.

We present a method to verify the correctness of parallel programs that perform complex numerical computations, including computations involving floating-point arithmetic. The method requires that a sequential version of the program be provided, to serve as the specification for the parallel one. The key idea is to use model checking, together with symbolic execution, to establish the equivalence of the two programs.

Property specifications concisely describe aspects of what a system is supposed to do. No matter what notation is used to describe them, however, it is difficult to represent these properties correctly, since there are often subtle, but important, details that need to be considered. Propel aims to guide users through the process of creating properties that are both accessible and mathematically precise, by providing templates for commonly-occurring property patterns. These templates explicitly represent these subtle details as options. In this paper, we present a new representation of these templates, a Question Tree that asks users a hierarchical sequence of questions about their intended properties. The Question Tree representation is particularly useful for helping users select the appropriate template, but it also complements the finite-state automaton and disciplined natural language representations provided by Propel. We also report on some case studies and on an experimental evaluation of the understandability of the disciplined natural language representation.

FLAVERS is a finite-state verification approach that allows an analyst to incrementally add constraints to improve the precision of the model of the system being analyzed. Except for trivial systems, however, it is impractical to compute which constraints should be selected to produce precise results for the least cost. Thus, constraint selection has been a manual task, guided by the intuition of the analyst. In this paper, we investigate several heuristics for selecting task automaton constraints, a kind of constraint that tends to reduce infeasible task interactions. We describe an experiment showing that one of these heuristics is extremely effective at improving the precision of the analysis results without significantly degrading performance.

One of the benefits of finite-state verification (FSV) tools, such as model checkers, is that a counterexample is provided when the property cannot be verified. Not all counterexamples, however, are equally useful to the analysts trying to understand and localize the fault. Often counterexamples are so long that they are hard to understand. Thus, it is important for FSV tools to find short counterexamples and to do so quickly. Commonly used search strategies, such as breadth-first and depth-first search, do not usually perform well in both of these dimensions. In this paper, we investigate heuristic-guided search strategies for the FSV tool FLAVERS and propose a novel two-stage counterexample search strategy. We describe an experiment showing that this two-stage strategy, when combined with appropriate heuristics, is extremely effective at quickly finding short counterexamples for a large set of verification problems.

This article describes FLAVERS, a finite-state verification approach that analyzes whether concurrent systems satisfy user-defined, behavioral properties. FLAVERS automatically creates a compact, event-based model of the system that supports efficient dataflow analysis. FLAVERS achieves this efficiency at the cost of precision. Analysts, however, can improve the precision of analysis results by selectively and judiciously incorporating additional semantic information into an analysis.We report on an empirical study of the performance of the FLAVERS/Ada toolset applied to a collection of multitasking Ada systems. This study indicates that sufficient precision for proving system properties can usually be achieved and that the cost for such analysis typically grows as a low-order polynomial in the size of the system.

Property specifications concisely describe what a software system is supposed to do. It is surprisingly difficult to write these properties correctly. There are rigorous mathematical formalisms for representing properties, but these are often difficult to use. No matter what notation is used, however, there are often subtle, but important, details that need to be considered. Propel aims to make the job of writing and understanding properties easier by providing templates that explicitly capture these details as options for commonly-occurring property patterns. These templates are represented using both "disciplined" natural language and finite-state automata, allowing the specifier to easily move between these two representations.

Finite-state verification is emerging as an important technology for proving properties about software. In our experience, we have found that analysts have different expectations at different times. When an analyst is in an exploratory mode, initially formulating and verifying properties, analyses usually find inconsistencies because of flaws in the properties or in the software artifacts being analyzed. Once an inconsistency is found, the analyst begins to operate in a fault-finding mode, during which meaningful counter-example traces are needed to help determine the cause of the inconsistency. Eventually, systems become relatively stable, but still require re-verification as evolution occurs. During such periods, the analyst is operating in a maintenance mode and would expect re-verification to usually report consistent results. Although it could be that one algorithm suits all three of these modes of use, the hypothesis explored in this paper is that each would be best served by an algorithm optimized for the expectations of the analyst.

Complex toolsets can be difficult to use. User interfaces can help by guiding users through the alternative choices that might be possible at any given time, but this tends to lock users into the fixed interaction models dictated by the user-interface designers. Alternatively, we propose an approach where the tool utilization model is specified by a process, written in a process definition langauge. Our approach incorporates a user-interface specification that describes how the user-interface is to respond to, or reflect, progress through the execution of the process definition. By not tightly binding the user-guidance process, the associated user-interfaces, and the toolset, it is easy to develop alternative processes that provide widely varying levels and styles of guidance and to be responsive to evolution in the processes, user interfaces, or toolset. In this paper, we describe this approach for developing process-driven user-guidance environments, a lossely coupled architecture for supporting this separation of concerns, and a generator for automatically binding the process and the user interface. We report on a case study using this approach. Although this case study used a specific process definition language and a specific toolset, the approach is applicable to other process definition languages and toolsets, provided they meet some basic, sound software engineering requirements.

Ever since formal verification was first proposed in the late sixties, the idea of being able to definitively determine if a program meets its specifications has been an appealing, but elusive, goal. Although verification systems based on theorem proving have improved considerably over the years, they are still inherently undecidable and require significant guidance from mathematically astute users. The human effort required for formal verification is so significant that it is usually only applied to the most critical software components.

It seems imperative that the complex processes that syner-gize humans and computers to solve widening classes of societal problems be subjected to rigorous analysis. One approach is to use a process definition language to spec-ify these processes and to then use analysis techniques to evaluate these definitions for important correctness proper-ties. Because humans demand flexibility in their participa-tion in complex processes, process definition languages must incorporate complicated control structures, such as various concurrency, choice, reactive control, and exception mecha-nisms. Well-designed process languages provide powerful abstractions for concise and precise specification of such control, but balance this with visualization support to help users also obtain intuitive insights. The underlying complex-ity of these control abstractions, however, often confounds these intuitions as well as complicates any analysis. Thus, the control abstraction complexity in process def-inition languages presents analysis challenges beyond those posed by traditional programming languages. This paper ex-plores some of the difficulties of analyzing process defini-tions. Specifically, we explore issues arising when applying the FLAVERS finite state verification system to processes written in the Little-JIL process definition language and il-lustrate these issues using a realistic ecommerce auction ex-ample. Although we employ a particular process definition language and analysis technique, our results seem more gen-erally applicable.

Traditionally, verification properties have been classified as safety or liveness properties. While this taxonomy has an attractive simplicity and is useful for identifying the appropriate analysis algorithm for checking a property, determining whether a property is safety, liveness, or neither can require significant mathematical insight on the part of the analyst. In this paper, we present an alternative property taxonomy. We argue that this taxonomy is a more natural classification of the kinds of questions that analysts want to ask. Moreover, most classes in our taxonomy have a known, direct mapping to the safety-liveness classification, and thus the appropriate analysis algorithm can be automatically determined.

The purpose of this panel is to introduce the Impact Project to the community, and to engage the community in a broad ranging discussion of the project's goals, approaches, and methods. Some of the project's early findings and directions will be presented.

In this paper we show how the FLAVERS data flow analysis technique, originally formulated for programs with the rendezvous model of concurrency, can be applied to concurrent Java programs. The general approach of FLAVERS is based on modeling a concurrent program as a flow graph and using a data flow analysis algorithm over this graph to check statically if a property holds on all executions of the program. The accuracy of this analysis can be improved by supplying additional information, represented as finite state automata, to the data flow analysis algorithm. In this paper we present a straightforward approach for modeling Java programs that uses the accuracy improving mechanism to represent the possible communications among threads in Java programs, instead of representing them directly in the flow graph model. We also discuss a number of error-prone thread communication patterns that can arise in Java and describe how FLAVERS can be used to check for the presence of these.

Partial order optimization techniques for distributed systems improve the performance of finite state verification approaches by avoiding redundant exploration of some portions of the state space. Previously, such techniques have been applied in the context of model checking approaches. In this paper we propose a partial order optimization of the program model used by FLAVERS, a data flow based finite state verification approach for checking user-specified properties of distributed software. We demonstrate experimentally that this optimization often leads to significant reductions in the run time of the analysis algorithm of FLAVERS. On average, for those cases where this optimization could be applied, we observed a speedup of 21%. For one of the cases, the optimization resulted in an analysis speedup of 91%.

As software engineering efforts move to more complex, distributed environments, coordinating the activities of people and tools becomes very important. While groupware systems address user level communication needs and distributed computing technologies address tool level communication needs, few attempts have been made to synthesize the common needs of both. This paper describes our attempt to do exactly that. We describe a framework for generating an agenda management system (AMS) from a specification of the system's requirements. The framework can meet a variety of requirements and produces a customized AMS appropriate for use by both humans and software tools. The framework and generated system support evolution in several ways, allowing existing systems to be extended as requirements change. We also describe our experiences using this approach to create an AMS to support a process programming environment.

Consistency management is important in many complex applications, but current languages and database systems inadequately support it. To address this limitation, we defined a consistency management model and incorporated it into the PLEIADES object management system. This paper illustrates some typical consistency management requirements and discusses the requirements in terms of both functionality and cross-cutting concerns that affect how this functionality is provided. It then describes the model and some design and implementation issues that arose in instantiating it. Finally, we discuss user feedback and future research plans.

FLAVERS, a tool for verifying properties of concurrent systems, uses composite data flow analysis to incrementally improve the precision of the results of its verifications. Although FLAVERS is one of the few static analysis techniques for concurrent systems that has the potential to handle large scale systems, it sometimes can still be very expensive to use. In this paper we experimentally compare the cost of two versions of this approach for solving composite data flow analysis problems. The first version, product-based, uses the more straightforward approach, and the second, tuple-based, is built around the idea of reducing analysis space requirements at the expense of analysis time. We demonstrate experimentally, by analyzing properties of actual concurrent programs, that the tuple-based version is comparable in time to the product-based version but for large composite data flow problems it requires several orders of magnitude less space.

In this demonstration we give a scenario of how FLAVERS, an implementation of the incremental accuracy improving data flow analysis approach [I], is used to verify event sequence properties of concurrent or distributed software programs.

Spurious results are an inherent problem of most static analysis methods. These methods, in an effort to produce conservative results, overestimate the executable behavior of a program. Infeasible paths and imprecise alias resolution are the two causes of such inaccuracies. In this paper we present an approach for improving the accuracy of Petri net-based analysis of concurrent programs by including additional program state information in the Petri net. We present empirical results that demonstrate the improvements in accuracy and, in some cases, the reduction in the search space that result from applying this approach to concurrent Ada programs.

In this paper we demonstrate the effectiveness of data flow analysis for verifying requirements of communication protocols. Data flow analysis is a static analysis method for increasing confidence in the correctness of software systems by automatically verifying that a given software artifact (e.g., design or code) must behave consistently with a specified requirement. In this case study, we apply the FLAVERS data flow analysis tool to pseudocode designs of the three way handshake connection establishment protocol and of the alternating bit protocol and prove that the behavior of the pseudocode is consistent with protocol behavioral requirement specifications. We show how FLAVERS is a particularly effective because it is computationally inexpensive, requires minimal human interaction, and is a general approach that can be applied incrementally until the desired accuracy is achieved. In addition, we show how assumptions about the environment in which a software system is executed can be incorporated into the analysis, using message losses as an example. We present experimental results and derive some guidelines about the classes of protocol requirement specifications that may be amenable to verification using FLAVERS.

Although event-based software integration is one of the most prevalent approaches to loose integration, no consistent model for describing it exists. As a result, there is no uniform way to discuss event-based integration, compare approaches and implementations, specify new event-based approaches, or match user requirements with the capabilities of event-based integration systems. We attempt to address these shortcomings by specifying a generic framework for event-based integration , the EBI framework, that provides a flexible, object-oriented model for discussing and comparing event-based integration approaches. The EBI framework can model dynamic and static specification, composition, and decomposition and can be instantiated to describe the features of most common event-based integration approaches. We demonstrate how to use the framework as a reference model by comparing and contrasting three well-known integration systems: FIELD, Polylith, and CORBA.

We explore a property-independent, coarsened, multilevel representation for supporting state reachability analysis for a number of different properties. This multilevel representation comprises a reachability graph derived from a highly optimized Petri net representation that is based on task interaction graphs and associated property-specific summary information. This highly optimized representation reduces the size of the reachability graph but may increase the cost of the analysis algorithm for some types of analyses. We explore this tradeoff. To this end, we have developed a framework for checking a variety of properties of concurrent programs using this optimized representation and present empirical results that compare the cost to an alternative Petri net representation. In addition, we present reduction techniques that can further improve the performance and yet still preserve analysis information. Although worst-case bounds for most concurrency analysis techniques are daunting, we demonstrate that the techniques that we propose significantly broaden the applicability of reachability analyses.

This paper presents a compactPetri net representa-

Classification D.2.4 Software/Program Verification, D.1.3 Concurrent Programming This paper describes FLAVERS, a finite-state verification approach that analyzes whether concurrent systems satisfy user-defined, behavioral properties. FLAVERS automatically creates a compact, event-based model of the system that supports efficient data-flow analysis. FLAVERS achieves this efficiency at the cost of precision. Analysts, however, can improve the precision of analysis results by selectively and judiciously incorporating additional semantic information into an analysis. We report on an empirical study of the performance of the FLAVERS/Ada toolset applied to a collection of multitasking Ada systems. This study indicates that sufficient precision for proving system properties can usually be

RELAY is a model of how a fault causes a failure on execution of some test datum. This process begins with introduction of an original state potential failure at a fault location and continues as the potential failure(s) transfers to output. Here we describe the second stage of this process, transfer of an incorrect intermediate state from a faulty statement to output.

Software engineering environments impose challenging requirements on the design and implementation of an object management system. Existing object management systems have been limited in both the kinds of functionality they have provided and in the models of support they define. This paper describes a system, called PLEIADES, which provides many of the object management capabilities required to support software engineering environments.

Although prototyping has long been touted as a potentially valuable software engineering activity, it has never achieved widespread use by developers of large-scale, production software. This is probably due in part to an incompatibility between the languages and tools traditionally available for prototyping (e.g., LISP or Smalltalk) and the needs of large-scale-software developers, who must construct and experiment with large prototypes. The recent surge of interest in applying prototyping to the development of large-scale, production software will necessitate improved prototyping languages and tools appropriate for constructing and experimenting with large, complex prototype systems. We explore techniques aimed at one central aspect of prototyping that we feel is especially significant for large prototypes, namely that aspect concerned with the definition of data objects. We characterize and compare various techniques that might be useful in defining data objects in large prototype systems, after first discussing some distinguishing characteristics of large prototype systems and identifying some requirements that they imply. To make the discussion more concrete, we describe our implementations of three techniques that represent different possibilities within the range of object definition techniques for large prototype systems.

A formal, general model of program dependences is presented and used to evaluate several dependence-based software testing, debugging, and maintenance techniques. Two generalizations of control and data flow dependence, called weak and strong syntactic dependence, are introduced and related to a concept called semantic dependence. Semantic dependence models the ability of a program statement to affect the execution behavior of other statements. It is shown that weak syntactic dependence is a necessary but not sufficient condition for semantic dependence and that strong syntactic dependence is necessary but not sufficient condition for a restricted form of semantic dependence that is finitely demonstrated. These results are used to support some proposed uses of program dependences, to controvert others, and to suggest new uses.>

A representation for concurrent programs, called task inter-action graphs, is presented. Task interaction graphs divide a program into maximal sequential regions connected by edges rep-resenting task interactions. This representation is illustrated and it is shown how it can be used to create concurrency graph rep-resentations that are much smaller than those created from con-trol flow graph representations. Both task interaction graphs and their corresponding concurrency graphs facilitate analysis of concurrent programs. Some analyses and optimizations on these representations are also described. 1

The authors report on the results of their evaluation of path-selection criteria based on data-flow relationships. They show how these criteria relate to each other, thereby demonstrating some of their strengths and weaknesses. A subsumption hierarchy showing their relationship is presented. It is shown that one of the major weaknesses of all the criteria is that they are based solely on syntactic information and do not consider semantic issues such as infeasible paths. The authors discuss the infeasible-path problem as well as other issues that must be considered in order to evaluate these criteria more meaningfully and to formulate a more effective path-selection criterion.>

The AdaPIC tool set, an important component of an Ada software development environment, is discussed. The AdaPIC tool set is one particular instantiation, specifically adapted for use with Ada, of the more general collection of language features and analysis capabilities that constitute the PIC approach to describing and analyzing relationships among software system components. This tool set is being tailored to support an incremental approach to the interface control aspects of the software development process. Following a discussion of the PIC interface control and incremental development concepts, the AdaPIC tool set is described, concentrating on its analysis tools and support for incremental development and demonstrating how it contributes to the technology for developing large Ada software systems.>

A formal model for describing and evaluating visibility control mechanisms is introduced. The model reflects a general view of visibility in which the concepts of requisition of access and provision of access are distinguished. This model provides a means for characterizing and reasoning about the various properties of visibility control mechanisms. Specifically, the notion of preciseness is defined. The utility of the model is illustrated by using it to evaluate and compare the relative strengths and weaknesses, with respect to preciseness, of the visibility control mechanisms found in Algol 60, Ada, Gypsy, and an approach called PIC, which specifically addresses the concerns of visibility control in large software systems.>

The partition analysis method compares a procedure's implementation to its specification, both to verify consistency between the two and to derive test data. Unlike most verification methods, partition analysis is applicable to a number of different types of specification languages, including both procedural and nonprocedural languages. It is thus applicable to high-level descriptions as well as to low-level designs. Partition analysis also improves upon existing testing criteria. These criteria usually consider only the implementation, but partition analysis selects test data that exercise both a procedure's intended behavior (as described in the specifications) and the structure of its implementation. To accomplish these goals, partition analysis divides or partitions a procedure's domain into subdomains in which all elements of each subdomain are treated uniformly by the specification and processed uniformly by the implementation. This partition divides the procedure domain into more manageable units. Information related to each subdomain is used to guide in the selection of test data and to verify consistency between the specification and the implementation. Moreover, the testing and verification processes are designed to enhance each other. Initial experimentation has shown that through the integration of testing and verification, as well as through the use of information derived from both the implementation and the specification, the partition analysis method is effective for evaluating program reliability. This paper describes the partition analysis method and reports the results obtained from an evaluation of its effectiveness.

White and Cohen have proposed the domain testing method, which attempts to uncover errors in a path domain by selecting test data on and near the boundary of the path domain. The goal of domain testing is to demonstrate that the boundary is correct within an acceptable error bound. Domain testing is intuitively appealing in that it provides a method for satisfying the often suggested guideline that boundary conditions should be tested.

Formatted input-output is available in a number of programming languages. In the most general case, the correspondence between data items and format items cannot be determined during compilation, and so it is determined dynamically during execution. However, in most pairs of data and format lists that occur in practice, determination of the correspondence is in fact possible during compilation. Although some commercial compilers make this determination, there is little published literature on the subject. In this paper, we briefly examine three areas in which compile-time determination of the data-format correspondence is useful: optimization, program validation, and automatic test data generation. A formalism for stating the problem is given, and a solution is discussed in terms of formal language theory. Using this formalism, an algorithm for determining the correspondence is given, and its application is illustrated by examples in both PL/I and Fortran.

An overview of some of the current program validation techniques is given. Though a variety of such techniques exist, it is now commonly agreed that program testing is an essential part of the program development process. Two testing methodologies, functional and structural, are described and a case made for combining both methodologies. Finally, a system that aids in structural testing is described.

This paper describes a system that attempts to generate test data for programs written in ANSI Fortran. Given a path, the system symbolically executes the path and creates a set of constraints on the program's input variables. If the set of constraints is linear, linear programming techniques are employed to obtain a solution. A solution to the set of constraints is test data that will drive execution down the given path. If it can be determined that the set of constraints is inconsistent, then the given path is shown to be nonexecutable. To increase the chance of detecting some of the more common programming errors, artificial constraints are temporarily created that simulate error conditions and then an attempt is made to solve each augmented set of constraints. A symbolic representation of the program's output variables in terms of the program's input variables is also created. The symbolic representation is in a human readable form that facilitates error detection as well as being a possible aid in assertion generation and automatic program documentation.