Search

In this paper, we propose a means to enhance an architecture description language with a description of component behavior. A notation-used for this purpose should be able to express the "interplay" on the component's interfaces and reflect step-bystep refinement of the component's specification during its design. In addition, the notation should be easy to comprehend and allow for formal reasoning about the correctness of the specification refinement and also about the correctness of an implementation in terms of whether it adheres to the specification. Targeting all these requirements together, the paper proposes employing behavior protocols which are based on a notation similar to regular expressions. As proof of the concept, the behavior protocols are used in the SOFA architecture description language at three levels: interface, frame, and architecture. Key achievements of this paper include the definitions of bounded component behavior and protocol conformance relation. Using these concepts, the designer can verify the adherence of a component's implementation to its specification at runtime, while the correctness of refining the specification can be verified at design time. [ABSTRACT FROM AUTHOR]

A global checkpoint is a set of local checkpoints, one per process. The traditional consistency criterion for global checkpoints states that a global checkpoint is consistent if it does not include messages received and not sent. This paper investigates other consistency criteria, transitlessness, and strong consistency. A global checkpoint is transitless if it does not exhibit messages sent and not received. Transitlessness can be seen as a dual of traditional consistency. Strong consistency is the addition of transitlessness to traditional consistency. The main result of this paper is a statement of the necessary and sufficient condition answering the following question: "Given an arbitraiy set of local checkpoints, can this set be extended to a global checkpoint that satisfies P" (where P is traditional consistency, transitlessness, or strong consistency). From a practical point of view, this condition, when applied to transitlessness, is particularly interesting as it helps characterize which messages do not need to be recorded by checkpointing protocols. [ABSTRACT FROM AUTHOR]

This paper discusses the problems that a software development organization must address in order to assess and improve its software processes. In particular, the authors are involved in a project aiming at assessing and improving the cur- rent practice and the quality manual of the Business Unit Telecommunications for Defense (BUTD) of a large telecommunications company. The paper reports on the usage of formal process modeling languages to detect inconsistencies, ambiguities, incompleteness, and opportunities for improvement of both the software process and its documentation. [ABSTRACT FROM AUTHOR]

This paper describes the design and implementation of an intelligent tutoring system for the Dijkstra-Gries programming methodology as defined by Cries in "The Science of Programming"[12]. The first part of the paper identifies the requirements of intelligent tutoring systems in general and those of the methodology in particular. It shows the suitability of the Smalltalk environment for developing expandable intelligent systems and the compatibility of Smalltalk's object-oriented paradigm with the Gries methodology's goal/plan approach to programming. We then describe how these requirements are met: an overview of the system's support of the methodology and the modules that enable the system to respond intelligently. As an example, a reusable tutorial part is presented, first from a student's perspective, then from an author's perspective. Finally the results of an evaluation of the system drawn from actual student experience are presented. [ABSTRACT FROM AUTHOR]

Mathematical software is devoted to solve problems involving matrix computation and manipulation. The main problem limiting the reusability of existing mathematical software is the following: programs are often not initially designed for being reused. Therefore, it is hard to find programs that can be easily reused. In the first part of this paper, we give a programming methodology useful for designing and implementing reusable code. We name unit a portion of code designed and implemented for being reused. Our units are self-contained software components featuring a high degree of information hiding. This way of organizing software facilitates the reuse process and, furthermore, improves the understandability of units. To speed up the implementation process, a system supporting the reusability of units from an existing software library is particularly useful. In the second part of this paper, we report about an easy to use system of this kind. [ABSTRACT FROM AUTHOR]

RELAY is a model of faults and failures that defines failure conditions, which describe test data for which execution will guarantee that a fault originates erroneous behavior that also transfers through computations and information flow until a failure is revealed. This model of fault detection provides a framework within which other testing criteria's capabilities can be evaluated. In this paper, we analyze three test data selection criteria that attempt to detect faults in six fault classes. This analysis shows that none of these criteria is capable of guaranteeing detection for these fault classes and points out two major weaknesses of these criteria. The first weakness is that the criteria do not consider the potential unsatisfiability of their rules; each criterion includes rules that are sufficient to cause potential failures for some fault classes, yet when such rules are unsatisfiable, many faults may remain undetected. Their second weakness is failure to integrate their proposed rules; although a criterion may cause a subexpression to take on an erroneous value, there is no effort made to guarantee that the intermediate values cause observable, erroneous behavior. This paper shows how the RELAY model overcomes these weaknesses. [ABSTRACT FROM AUTHOR]

The selection of appropriate test cases is an important issue for conformance testing of protocol implementations as well as in software engineering. A number of methods are known for the selection of a test suite based on the specification of the implementation under test, assumed to be given in the form of a finite state machine. This paper presents a new method which provides a logical link between several of the known methods. Called the "partial W method," it has general applicability, full fault-detection power, and yields shorter test suites than the W method. The second part of the paper discusses various other issues which have an impact on the selection of a suitable test suite. This includes the consideration of interaction parameters, various test architectures for protocol testing, and the fact that many specifications do not satisfy the assumptions made by most test selection methods, such as complete definition, a correctly implemented reset function, a limited number of states in the implementation, and determinism. [ABSTRACT FROM AUTHOR]

This paper proposes a new lower bound on the number of processors and finish time for the problem of scheduling precedence graphs with communication costs. An algorithm (ETF) has been proposed by Hwang [1] for scheduling precedence graphs In systems with interprocessor communication limes. In this paper the notion of the earliest starting time of a task is formulated for the context of lower bounds. A lower bound on the completion time is proposed. A task delay which does not increase the earliest completion time of a schedule is defined. Each task can then be scheduled within a time interval without affecting the lower bound performance on the finish time. This leads to definition of a new lower bound on the number of processors required to process the task graph. A derivation of the minimum time increase over the earliest completion time is also proposed for the case of smaller number of processors. Finally the paper proposes a lower bound on the minimum number of interprocessor communication links required to achieve optimum performance. Evaluation has been carried out by using a set of 360 small graphs. The bound on the finish time deviates at most by 5% from the optimum solution in 96% of the cases and performs well with respect to the minimum number of processors and communication links. [ABSTRACT FROM AUTHOR]

A basic requirement for communication in a heterogeneous computing environment is a standard external data representation. Abstract Syntax Notation One (ASN.1) has been widely used in international standard specifications; its transfer-syntax, the Basic Encoding Rules (BER), is used as the external data representation. This paper presents a HER implementation called the ED library. The ED library includes a number of encoding and decoding routines that may be used as primitive functions to compose encoders and decoders for arbitrarily complicated ASN.1 data-types. Based on the ED library, an ASN.1-C compiler, called CASN1, is designed and implemented to free the protocol implementors from the arduous work of translating protocol-defined data-types and constructing their encoders and decoders. Given an ASN.1 protocol specification, CASNI automatically translates the input ASN.1 modules into C and generates the BER encoders and decoders for the protocol defined data-types. This paper discusses the CASN1 design principles, user interface, and some example applications. The performance of the ED library and generated CASN1 code is also measured and discussed. [ABSTRACT FROM AUTHOR]

In the event-action model of interactions between the debugging system and the program being debugged, an event will occur on the evaluation of a conditional defined in terms of the program activity if the evaluation yields the value true, and an action is an operation performed by the debugging system on the occurrence of an event. This paper presents a set of mechanisms for expressing conditionals at different levels of abstraction. At the lowest level, we have the simple conditionals, which can be expressed in terms of the values of the pro- gram entities and of the execution of the program statements. Simple conditionals can be grouped to form higher-level compound conditionals, which can be expressed in terms of the state and flow histories. The paper shows that the proposed abstraction mechanisms are powerful tools for monitoring program activity. They adequately support different debugging techniques, and offer the user a considerable degree of control over the debugging experiment. [ABSTRACT FROM AUTHOR]

SLAN-4 ("Software Language-4") was developed to meet the need for a formal tool for specifying and designing large software systems. It provides language constructs for algebraic and axiomatic specifications and also pseudocode constructs for the design step. A major design goal was to ease subsequent refinements of a (given) specification. The design can start with a very informal specification, which can be implemented later using lower level concepts. This paper gives an overview of the SLAN-4 syntax and semantics. It concentrates on the most important aspects of: • abstract data types, • algebraic specification of abstract data types, and • axiomatic specification of modules. Because the pseudocode part of SLAN-4 consists mainly of control structures similar to those in modern high-level programming languages, this element of the language is not separately described. The paper includes an example of how to use SLAN-4, and also the experiences gained in using the language to formally specify a real-world software product of about 18 000 lines of code written in an IBM internal high-level language. [ABSTRACT FROM AUTHOR]

In the area of software development, data processing management often focuses more on coding techniques and system architecture than on how to manage the development. In recent years, "structured programming" and "structured analysis" have received more attention than the techniques software managers employ to manage. Moreover, these coding and architectural considerations are often advanced as the key to a smooth running, well managed project. This paper documents a philosophy for software development and the tools used to support it. Those management techniques deal with quantifying such abstract terms as "productivity," "performance," and "progress," and with measuring these quantities and applying management controls to maximize them. The paper also documents the application of these techniques on a major software development effort. [ABSTRACT FROM AUTHOR]

This paper, which was initially prepared to accompany a series of lectures given at the 1978 NATO International Summer School on Program Construction, is primarily tutorial in nature. It begins by discussing in a general setting the role of type abstraction and the need for formal specifications of type abstractions. It then proceeds to examine in some detail two approaches to the construction of such specifications: that proposed by Hone in his 1972 paper "Proofs of Correctness of Data Representations," and the author's own version of algebraic specifications. The Hoare approach is presented via a discussion of its embodiment in the programming language Euclid. The discussion of the algebraic approach includes material abstracted from earlier papers as well as some new material that has yet to appear. This new material deals with parameterized types and the specification of restrictions. The paper concludes with a brief discussion of the relative merits of the two approaches to type abstraction. [ABSTRACT FROM AUTHOR]

Recent advances in technology have made the construction of general-purpose systems out of many small independent microprocessors feasible. One of the issues concerning distributed systems is the question of appropriate language constructs for the handling of communication and synchronization. In his paper, "Communicating sequential processes," Hoare has suggested the use of the input and output constructs and Dijkstra's guarded commands to handle these two issues. This paper examines Hoare's concepts in greater detail by concentrating on the following two issues: 1) allowing both input and output commands to appear in guards, 2) simple abstract implementation of the input and output constructs. In the process of examining these two issues we develop a framework for the design of appropriate communication and synchronization facilities for distributed systems. [ABSTRACT FROM AUTHOR]

This paper presents a method for automatically analyzing loops, and discusses why it is a useful way to look at loops. The method is based on the idea that there are four basic ways in which the logical structure of a loop is built up. An experiment is presented which shows that this accounts for the structure of a large class of loops. The paper discusses how the method can be used to automatically analyze the structure of a loop, and how the resulting analysis can be used to guide a proof of correctness for the loop. An automatic system is described which performs this type of analysis. The paper discusses the relationship between the structure building methods presented and programming language constructs. A system is described which is designed to assist a person who is writing a program The intent is that the system will cooperate with a programmer throughout all phases of work on a program and be able to communicate with the programmer about it. [ABSTRACT FROM AUTHOR]

Debugging often involves 1) finding the point of failure (the first statement that produces bad output) and 2) finding and fixing the actual bug. Print statements and debugger break points can help with step 1. Slicing the program back from values used at the point of failure can help with step 2. However, neither approach is ideal: Debuggers and print statements can be clumsy and timeconsuming and backward slices can be almost as large as the original program. This paper addresses both problems. We present callstack-sensitive slicing, which reduces slice sizes by leveraging the series of calls active when a program fails. We also show how slice intersections may further reduce slice sizes. We then describe a set of tools that identifies points of failure for programs that produce bad output. Finally, we apply our point-of-failure tools to a suite of buggy programs and evaluate callstack-sensitive slicing and slice intersection as applied to debugging. Callstack-sensitive slicing is very effective: On average, a callstack-sensitive slice is about 0.31 time the size of the corresponding full slice, down to just 0.06 time in the best case. Slice intersection is less impressive, on average, but may sometimes prove useful in practice. [ABSTRACT FROM AUTHOR]

Design patterns are generic design solutions that can be applied and composed in different applications where pattern-related information is generally implicit in the Unified Modeling Language (UML) diagrams of the applications. It is unclear in which pattern instances each modeling element, such as class, attribute, and operation, participates. It is hard for a designer to find the design patterns used in an application design. Consequently, the benefits of design patterns are compromised because designers cannot communicate with each other in terms of the design patterns they used and their design decisions and trade-offs. In this paper, we present a UML profile that defines new stereotypes, tagged values, and constraints for tracing design patterns in UML diagrams. These new stereotypes and tagged values are attached to a modeling element to explicitly represent the role the modeling element plays in a design pattern so that the user can identify the pattern in a UML diagram. Based on this profile, we also develop a Web service (tool) for explicitly visualizing design patterns in UML diagrams. With this service, users are able to visualize design patterns in their applications and compositions because pattern-related information can be dynamically displayed. A real-world case study and a comparative experiment with existing approaches are conducted to evaluate our approach. [ABSTRACT FROM AUTHOR]

Abstract--Functional refinement is beneficial to Object-Oriented (OO) software development, especially for problems with more complex functions. However, the use of functional refinement in OO software development has not received much attention. This paper proposes an enhanced data flow diagram (DFD), called data flow net (DF net), for specifying use-cases through functional decomposition. It proposes a novel approach to complement existing OO software development methods with functional decomposition for realizing use-cases, especially those with more complex functions. In the requirements analysis stage, the proposed approach realizes use-cases through functional refinement and specifies them in DF nets. In the design and implementation stages, it transforms the DF nets systematically and precisely into OO design and implementation. The approach is amenable to automation and a prototype has been developed to support the transformation process. In the development of an OO system, it is seamless to realize some of the use-cases using the proposed approach and the remaining use-cases in the same target system using any existing OO software development methods. [ABSTRACT FROM AUTHOR]

Requirements engineering's continuing dependence on natural language description has made it the focus of several efforts to apply language engineering techniques. The raw textual material that forms an input to early phase requirements engineering and which informs the subsequent formulation of the requirements is inevitably uncontrolled and this makes its processing very hard. Nevertheless, sufficiently robust techniques do exist that can be used to aid the requirements engineer provided that the scope of what can be achieved is understood. In this paper, we show how combinations of lexical and shallow semantic analysis techniques developed from corpus linguistics can help human analysts acquire the deep understanding needed as the first step towards the synthesis of requirements. [ABSTRACT FROM AUTHOR]

Using design patterns is claimed to improve programmer productivity and software quality. Such improvements may manifest both at construction time (in faster and better program design) and at maintenance time (in faster and more accurate program comprehension). This paper focuses on the maintenance context and reports on experimental tests of the following question: Does it help the maintainer if the design patterns in the program code are documented explicitly (using source code comments) compared to a well-commented program without explicit reference to design patterns? Subjects performed maintenance tasks on two programs ranging from 360 to 560 LOC including comments. Both programs contained design patterns. The controlled variable was whether the use of design patterns was documented explicitly or not. The experiments thus tested whether pattern comment lines (PCL) help during maintenance if patterns are relevant and sufficient program comments are already present. It turns out that this question is a challenge for the experimental methodology: A setup leading to relevant results is quite difficult to find. We discuss these issues in detail and suggest a general approach to such situations. The experiment was performed with Java by 74 German graduate students and then repeated with C++ by 22 American undergraduate students. A conservative analysis of the results supports the hypothesis that pattern-relevant maintenance tasks were completed faster or with fewer errors if redundant design pattern information was provided. Redundant means that the information carried in pattern comments is also available in different form in other comments. The contribution of this article is twofold: It provides the first controlled experiment results on design pattern usage and it presents a solution approach to an important class of experiment design problems for experiments regarding documentation. [ABSTRACT FROM AUTHOR]

Static analysis of concurrent programs has been hindered by the well known state explosion problem. Although many different techniques have been proposed to combat this state explosion, there is little empirical data comparing the performance of the methods. This information is essential for assessing the practical value of a technique and for choosing the best method for a particular problem. In this paper, we carry out an evaluation of three techniques for combating the state explosion problem in deadlock detection: reachability search with a partial order state space reduction, symbolic model checking, and inequality necessary conditions. We justify the method used for the comparison, and carefully analyze several sources of potential bias. The results of our evaluation provide valuable data on the kinds of programs to which each technique might best be applied. Furthermore, we believe that the methodological issues we discuss are of general significance in comparison of analysis techniques. [ABSTRACT FROM AUTHOR]

A key index of the performance of a rule-based pro- gram used in real-time monitoring and control is its response time, defined by the longest program execution time before a fixed point of the program is reached from a start state. Previous work in computing the response-time bounds for rule-based programs effectively assumes that all rules take the same amount of firing time, It is also assumed that if two rules are enabled, then either one of them may be scheduled first for firing. These assumptions can result in loose bounds, especially in the case programmers choose to impose a priority structure on the set of rules. In this paper, we remove the uniform-firing-cost assumption and discuss how to get tighter bounds by taking rule-priority information into account. We show that the rule-suppression relation we previously introduced can be extended to incorporate rule-priority information. A bound-derivation algorithm for programs whose potential-trigger relations satisfy an acyclicity condition is presented, followed by its correctness proof and an analysis example. [ABSTRACT FROM AUTHOR]

Limiting the extent of error propagation when faults occur and localizing the subsequent error recovery are common concerns in the design of fault tolerant parallel processing systems. Both activities are made easier if the designer associates fault tolerance mechanisms with the underlying atomic actions of the system. With this in mind, this paper has investigated two methods for the identification of atomic actions in parallel processing systems described using CSP. Explicit trace evaluation forms the basis of the first algorithm, which enables a designer to analyze interprocess communications and thereby locate atomic action boundaries in a hierarchical fashion. The second method takes CS? descriptions of the parallel processes and uses structural arguments to infer the atomic action boundaries. This method avoids the difficulties involved with producing full trace sets, but does incur the penalty of a more complex algorithm. [ABSTRACT FROM AUTHOR]

In this paper we introduce a novel technique, the scheduler luck game (in short sl-game) for analyzing the performance of randomized distributed protocols. We apply it in studying uniform self-stabilizing protocols for leader election under read/write atomicity. We present two protocols for the case where each processor in the system can communicate with all other processors and analyze their performance using the sl-game technique. [ABSTRACT FROM AUTHOR]

Weyuker and Jeng have investigated the conditions that affect the performance of partition testing and have compared analytically the fault-detecting ability of partition testing and random testing. This paper extends and generalizes some of their results. We give more general ways of characterizing the worst case for partition testing, along with a precise characterization of when this worst case is as good as random testing. We also find that partition testing is guaranteed to perform at least as well as random testing so long as the number of test cases selected is in proportion to the size of the subdomains. [ABSTRACT FROM AUTHOR]

In this paper, we present a specification language for real-time systems called Modechart. The semantics of Modechart is given in terms of RTL (Real Time Logic [8]) that is especially amenable to reasoning about the absolute (real-time clock) timing of events. The semantics of Modechart has an important property that the translation of a Modechart specification into RTL formulas will result in a hierarchical organization of the resulting RTL assertions. This gives us significant leverage in reasoning about properties of a system by allowing us to filter out assertions that concern lower levels of abstraction. Some results about desirable properties of Modechart specifications will be given. A graphical implementation of Modechart has been completed. [ABSTRACT FROM AUTHOR]

Quorum attainment protocols are an important part of many mutual exclusion algorithms. Assessing the performance of such protocols in terms of number of messages, as is usually done, may be less significant than being able to compute the delay in attaining the quorum. Some protocols achieve higher reliability at the expense of increased message cost or delay. A unified analytical model which takes into account the network delay and its effect on the time needed to obtain a quorum is presented. A combined performability metric, which takes into account both availability and delay, is defined in this paper, and expressions to calculate its value are derived for two different reliable quorum attainment protocols: Agrawal and El Abbadi's and Majority Consensus algorithms. Expressions for the Primary Site approach are also given as upper bound on performability and lower bound on delay. A parallel version of the Agrawal and El Abbadi protocol is introduced and evaluated. This new algorithm is shown to exhibit lower delay at the expense of a negligible increase in the number of messages exchanged. Numerical results derived from the model are discussed [ABSTRACT FROM AUTHOR]

This paper presents a method for the modular specification and verification of data abstractions in which multiple abstract objects share a common realization level data structure. Such shared realizations are an important implementation technique for data abstractions, because they provide for efficient use of memory; i.e., they allow the amount of memory allocated to the realization of an abstract object to be dynamic, so that only the amount of memory needed for its realization is allocated to it at any one time. To be explicit, an example of this kind of data abstraction is given. Although a number of programming languages provide good support for shared realizations, there has been limited research on its specification and verification. An important property of our method is that it allows data abstractions to be dealt with modularly; i.e., each data abstraction can be specified and verified individually. Its abstract specification is made available for use by other program modules, but all of its implementation details are hidden, which simplifies the verification of code that uses the abstraction. We have developed semantics for data abstractions and our method of specification, and have used it to prove that our verification method is logically sound and relatively complete in the sense of Cook [7]. The use of shared realizations impacts specification and verification in several related ways. The manipulation of one abstract object may inadvertently produce a side effect on other abstract objects. Without shared realizations, such unwanted side effects can be prevented by scoping rules, but this is not possible with shared realizations. Instead, the absence of such side effects must be explicitly proven by the verification method. This requires the specification language to provide for quantification over the currently active (allocated) instances of an abstract type that is not necessary for the specification of less advanced implementations of data abstractions. [ABSTRACT FROM AUTHOR]

This paper presents four optimization models to demonstrate that the optimization of software reliability within the available resources can be accomplished. The models help us find the optimal software system structure while considering basic information on reliability and cost of modules. Each model is applicable to a distinct situation. All four models maximize reliability while ensuring that expenditures remain within budget. [ABSTRACT FROM AUTHOR]

Fault injection has been used to evaluate the dependability of computer systems, but most fault-injection studies concentrate on the final impact of faults on the system with an emphasis on fault latency and coverage issues. What realty happens after a fault is injected and how a fault propagates in a software system are not well understood. This paper presents a fault injection and monitoring environment (FINE) as a tool to study fault propagation in the UNIX kernel. FINE injects hardware-induced software errors and software faults into the UNIX kernel and traces the execution flow and key variables of the kernel. It consists of a fault injector, a software monitor, a workload generator, a controller, and several analysis utilities. Experiments on SunOS 4.1.2 are conducted by applying FINE to investigate fault propagation and to evaluate the impact of various types of faults. Fault propagation models are built for both hardware and software faults. Transient Markov reward analysis is performed based on the models to evaluate the loss of performance due to an injected fault. Experimental results show that memory faults and software faults usually have a very long latency while bus faults and CPU faults tend to crash the system immediately. About half of the detected errors are data faults, which are detected when the system tries to access an unauthorized memory location. Only about 8% of faults propagate to other UNIX subsystems. Markov reward analysis shows that the performance loss incurred by bus faults and CPU faults is much higher than that incurred by software and memory faults. Among software faults, the impact of pointer faults is higher than that of nonpointer faults. [ABSTRACT FROM AUTHOR]

Applying equal testing and verification effort to all parts of a software system is not very efficient, especially when resources are limited and scheduling is tight. Therefore, one needs to be able to differentiate low/high fault frequency components so that testing/verification effort can be concentrated where needed. Such a strategy is expected to detect more faults and thus improve the resulting reliability of the overall system. This paper presents the Optimized Set Reduction approach for constructing such models, intended to fulfill specific software-engineering needs. Our approach to classification is to measure the software system and build multivariate stochastic models for predicting high-risk system components. We present experimental results obtained by classifying Ada components into two classes: is or is not likely to generate faults during system and acceptance test. Also, we evaluate the accuracy of the model and the insights it provides into the error-making process. [ABSTRACT FROM AUTHOR]

A new approach for checkpointing and rollback recovery in a distributed computing system using a common time base is proposed in this paper. First, a common time base is established in the system using a hardware clock synchronization algorithm. This common time base is coupled with the idea of pseudo-recovery points to develop a checkpointing algorithm that has the following advantages: 1) reduced wait for commitment for establishing recovery lines, 2) fewer messages to be exchanged, and 3) less memory requirement. These advantages are assessed quantitatively by developing a probabilistic model. [ABSTRACT FROM AUTHOR]

This paper examines several relations between software testing criteria, exploring whether for each relation R and each pair of criteria, C1 and C2, R(C1, C2) guarantees that C1 is better at detecting faults than C2 according to various probabilistic measures of fault-detecting ability. It is shown that the fact that C1 subsumes C2 does not guarantee that C1 is better at detecting faults. Relations that strengthen the subsumption relation and that have more bearing on fault-detecting ability are introduced. [ABSTRACT FROM AUTHOR]

We explain why pre-run-time scheduling is essential if one wishes to guarantee that timing constraints will be satisfied in a large complex hard-real-time system. We examine some of the major concerns in pre-run-time scheduling and consider what formulations of mathematical scheduling problems can be used to address those concerns. This paper provides a guide to the available algorithms. [ABSTRACT FROM AUTHOR]

We describe a technique and an environment- supporting specialization of generalized software components. The technique is based on symbolic execution. It allows one to transform a generalized software component into a more specific and more efficient component. Specialization is motivated as a technique that improves software reuse. The idea is that a library of generalized components exists and the environment supports a designer in customizing a generalized component when the need arises for reusing it under more restricted conditions. It is also justified as a re-engineering technique that helps optimize a program during maintenance. Specialization is supported by an interactive environment which provides several transformation tools: a symbolic executor/simplifier, an optimizer, and a loop refolder. The paper describes the conceptual basis for these transformation techniques, provides examples of their application, and outlines how they cooperate in a prototype environment for the Ada programming language. [ABSTRACT FROM AUTHOR]

This paper describes a method of semi-automatic specification refinement and program generation using library modules. Users write their specifications, modify and rearrange them so that the specifications can be refined with the aid of the library modules. When a specification is given, a refinement system called MAPS searches for library modules applicable to the given specification, replaces the specification with a more detailed description written in the operation part of the modules, and converts the refined specification into a program written in a programming language designated by the user. Case-like expressions or pseudo-natural language expressions are used for describing user's specifications and specifications for library modules. [ABSTRACT FROM AUTHOR]

The process of verifying that real-time software will meet its timing constraints, referred to as worst-case schedulability analysis, or simply schedulability analysis, is an essential part of the development of real-time software. Currently, real- time software programmers perform schedulability analysis in a manual, nonsystematic, error-prone way. Attempts to systematize schedulability analysis have so far resulted in techniques which can adequately model and analyze only simple real-time systems. When applied to realistic (and thus mostly nontrivial) real- time systems, these techniques result in overly pessimistic worst- case bounds. The failure of these existing schedulability analysis techniques applied to realistic systems can largely be attributed to their lack of detail. That is, practically all information about the language, its implementation, program organization, and hard- ware configuration is not taken into account or reduced to a small number of parameters. Thus usable techniques for systematic schedulability analysis are badly needed. These techniques need to take into account more information than the existing ones do, and produce good worst-case time bounds when applied to realistic real-time systems. In this paper we present a set of language-independent schedulability analysis techniques. Utilizing knowledge of implementation- and hardware-dependent information in a table-driven fashion, these techniques provide accurate worst-case time bounds and other schedulability information. A prototype schedulability analyzer has been developed to demonstrate the effectiveness of these techniques. The analyzer consists of a partially language- dependent front-end, targeted at Real-Time Euclid, a new real- time language specifically designed with a set of schedulability analysis provisions built-in, and a language-dependent back-end. The analyzer has been used on a number of realistic real-time programs, run on a multiple-microprocessor system. Predicted program performance differs only marginally from the actual performance. This is contrasted with an existing schedulability analysis method applied to the same programs. Predictions of this existing method deviate quite considerably from the actual performance. Thus our approach to schedulability analysis is effective and practical. [ABSTRACT FROM AUTHOR]

In this paper, we describe an approach for addressing the important problem of how long to test and debug software before it is released. Our approach is based on the principles of decision making under uncertainty, and involves a maximization of expected utility. We suggest two plausible forms for the utility function, one based on costs alone and the other involving the realized reliability of the software. Using results from the literature on probabilistic models for software failure, we outline, for the case of single state testing, the ensuing optimization problem which can be addressed using numerical techniques. The sensitivity of our results to the various input parameters is discussed and some directions for future research outlined. [ABSTRACT FROM AUTHOR]

Diagrams play a central role in software engineering. They are used for specifying design elements such as requirements, concurrent systems, database models and interactive systems. Families of diagrams form visual languages, and creating such diagrams constitutes visual programming. The Visual Programmer's WorkBench (VPW) addresses the rapid synthesis of programming environments for the specification, analysis, and execution of visual programs. A language-based environment for a specific visual language is generated in VPW from a specification of the syntactic structure, the abstract structure, the static semantics and the dynamic semantics of the language. VPW is built around a model of distributed processing based on shared distributed memory. This framework is used both in defining the architecture of the environment and for the execution model of visual languages. The Visual Programmer's WorkBench has been used to experiment with visual programming environments for several visual languages. This paper describes the design of the Visual Programmer's WorkBench and our experience using it to generate a distributed programming environment for a concurrent visual language. [ABSTRACT FROM AUTHOR]

The most important feature of visual languages is their ability to represent a user's mental concepts pictorially, thus providing for ease of learning and use. In order for this feature to be best exploited, there must be a close connection between the user's mental model of the application environment and the meaning of the icons in the system. Thus, a visual language must be accurately tuned to the application environment to which it is directed. This paper presents a system to generate and interpret customized visual languages in given application areas. The generation is highly automated. The user presents a set of sample visual sentences to the generator. The generator uses inference grammar techniques to produce a grammar that generalizes the initial set of sample sentences, and exploits general semantic information about the application area to determine the meaning of the visual sentences in the inferred language. The interpreter is modeled on an attribute grammar. A knowledge base, constructed during the generation of the system, is then consulted to construct the meaning of the visual sentence. The architecture of the whole system and its use in the application environment of visual text editing (inspired by the Heidelberg Icon Set) enhanced with file management features is reported. [ABSTRACT FROM AUTHOR]

This paper describes the Penelope verification editor and its formal basis. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich sub- set of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that we can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy. [ABSTRACT FROM AUTHOR]

This paper gives a formal specification of three base Avalon/C++ classes; recoverable, atomic, and subatomic. Programmers derive from class recoverable to define persistent objects, and from either class atomic or class subatomic to define atomic objects. The specifications, written in Larch, provide the means for showing that classes derived from the base classes implement objects that are persistent or atomic, and thus exemplify the applicability of an existing specification method to specifying "nonfunctional" properties. Writing these format specifications for Avalon/C++'s built-in classes has helped to clarify places in the programming language where features interact, to make unstated assumptions explicit, and to characterize complex properties of objects. [ABSTRACT FROM AUTHOR]

A state constraint is a new programming construct designed to restrict the domain of definition of a program. It can be used to decompose a program pathwise, i.e., to divide the program into subprograms along the control How, as opposed to divide the program across the control flow when the program is decomposed into functions and procedures. As a result one can now construct and manipulate a program consisting of one or more execution paths of another program. This paper describes the idea involved, examines the properties of state constraints, establishes a formal basis for pathwise decomposition, and discusses their utilities in program simplification, testing, and verification. [ABSTRACT FROM AUTHOR]

The programming tradeoffs between structure-oriented and clause-oriented operations on data structures in Prolog are limited in current implementations of Prolog, because the assertion of clauses that include uninstantiated variables destroys any binding between these variables and those with which they are unified in the execution of the program. In this paper, we propose new built-in predicates for Prolog that allow us to assert predicate variable pointers, which are constants, rather than uninstantiated variables. We show: 1) the possible performance benefits of clause-oriented implementations of data structures over equivalent structure-oriented versions, 2) the logical implications of the proposed built-in predicates, and 3) their practical significance by integrating them in C-Prolog, and evaluating the two different implementations of the symbol table dictionary in Warren's Pseudo-Pascal Compiler example. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of the dependability validation of fault-tolerant computing systems and more specifically the validation of the fault-tolerance mechanisms. The presented approach is based on the use of fault-injection at the physical level on a hardware/software prototype of the considered system. The place of this approach in a validation directed design process, as well as its place with respect to related works on fault-injection, is clearly identified. The major requirements and problems related to the development and application of a validation methodology based on fault injection are presented and discussed. Emphasis is put on the definition, analysis, and use of the experimental dependability measures that can be obtained. The proposed methodology has been implemented through the realization of a general pin-level fault injection tool (MESSALINE) and its usefulness is demonstrated by the application of MESSALINE to the experimental validation of two systems: 1) a subsystem of a centralized computerized inerlocking system for railway control applications and 2) a distributed system corresponding to the current implementation of the dependable communication system of the ESPRIT Delta-4 Project. [ABSTRACT FROM AUTHOR]

This paper shows how design time testing may be used in conjunction with formal specification. Emphasis is placed upon the benefits of using an executable specification language OBJ, a design controlled by requirements specification and adherence to the "regularity" and "uniformity" hypotheses in dynamic validation. Such an approach offers positive benefits by providing early design validation and a controlled, disciplined design process. [ABSTRACT FROM AUTHOR]

There is a need for widespread exchange of electronic documents in domains as diverse as book publishing, automated offices, factories, and research laboratories. The variety of data representations, and the subsequent need for data translation, is a major obstacle to this exchange. This paper describes a comprehensive data translation system with the following characteristics: 1) it is derived from a formal model of the translation task; 2) it supports the building of translation tools; 3) it supports the use of translation tools; and 4) it is accessible to its targeted end-users. A software architecture to achieve the translation capability is fully implemented. Translators have been generated using the architecture, both by the original software developers and by industrial associates who have installed the architecture at their own sites. [ABSTRACT FROM AUTHOR]

This paper introduces web structures and their transformations as a tool for representing and manipulating programs. The theory of web structures and web structure transformations is developed in the framework of the category theory. Once a program has been represented as a web structure, software tools, such as a high level data flow analyzer or other general program transformers, can be written as sets of web structure production rules. An implementation of web structure transformations, along the lines of [1], is in progress. On the other hand, the mathematical theory of web structure transformations allows formal proofs of properties both at the metatheoretical and theoretical levels. [ABSTRACT FROM AUTHOR]

We present a novel yet simple technology which enables customized database management systems to be developed rapidly. Over the last few years, a theory of database implementation was developed to explain the storage architectures of many commercial DBMS's (i.e., how these systems store and retrieve data) [5]. The theory identified basic components of DBMS software, required all components to have the same interface, and showed that component com- position can be achieved in a simple manner. We are designing an extensible DBMS, called GENESIS, which is based on this theory. This paper gives a detailed description of our first operational prototype. DBMS software components in GENESIS can be written in a few months. When all components for a target DBMS are present, writing the architecture specification of the DBMS and reconfiguring GENE- SIS takes a few hours and can be accomplished with negligible cost. Building the same DBMS from scratch can take many man-years and cost hundreds of thousands of dollars. We believe that the extensible software technology proposed herein embodies an important advance in tailoring database management systems to specialized applications. We also outline a way that our technology might impact software development beyond the confines of a DBMS setting. [ABSTRACT FROM AUTHOR]

A test data adequacy criterion is a predicate which is used to determine whether a program has been tested "enough." An adequacy criterion is applicable if for every program there exists a set of test data for the program which satisfies the criterion. Most test data adequacy criteria based on path selection fail to satisfy the applicability property because, for some programs with unexecutable paths, no adequate set of test data exists. In this paper, we extend the definitions of the previously introduced family of data flow testing criteria to apply to programs written in a large subset of Pascal. We then define a new family of adequacy criteria called feasible data flow testing criteria, which are derived from the data flow testing criteria. The feasible data flow testing criteria circumvent the problem of nonapplicability of the data flow testing criteria by requiring the test data to exercise only those definition-use associations which are executable. We show that there are significant differences between the relationships among the data flow testing criteria and the relationships among the feasible data flow testing criteria. We also discuss a generalized notion of the executability of a path through a program unit. A script of a testing session using our data flow testing tool, ASSET, is included in the Appendix. [ABSTRACT FROM AUTHOR]