Search

The article presents information on the 20th anniversary of the IEEE International Conference on Software Maintenance (ICSM). Software maintenance and evolution continues to play a vital role in the development of software systems. For many years there has been an international effort among researchers and practitioners to control the costs associated with software maintenance and evolution and to improve the quality of the processes and products associated with this vital activity. Software maintenance encompasses human elements of software engineering, which require psychological, statistical, and empirical evaluation. It involves algorithms, methods, and techniques which require a deep understanding of all activities in the software development life cycle. Since its inception in 1983, ICSM has evolved into an international forum for researchers, practitioners, educators, technology transfer experts, project managers, tool developers, and users who explore current issues facing the computing community. In 2004, the ICSM program chairs, Mark Harman from King's College in London and Bogdan Korel from Illinois institute of Technology in Chicago, selected 38 papers for inclusion in the proceedings from 122 submissions.

Analysis techniques, such as control flow, data flow, and control dependence, are used for a variety of software engineering tasks, including structural and regression testing, dynamic execution profiling, static and dynamic slicing, and program understanding. To be applicable to programs in languages such as Java and C++, these analysis techniques must account for the effects of exception occurrences and exception handling constructs; failure to do so can cause the analysis techniques to compute incorrect results and, thus, limit the usefulness of the applications that use them. This paper discusses the effects of exception handling constructs on several analysis techniques. The paper presents techniques to construct representations for programs with explicit exception occurrences-exceptions that are raised explicitly through throw statements-and exception handling constructs. The paper presents algorithms that use these representations to perform the desired analyses. The paper also discusses several software engineering applications that use these analyses. Finally, the paper describes empirical results pertaining to the occurrence of exception handling constructs in Java programs and their effect on some analysis tasks. [ABSTRACT FROM AUTHOR]

The article focuses on architecture-independent language and software tools for parallel processing. Parallel processing systems demonstrate their effectiveness as tools that deliver high-performance in solving complex problems. The concept of parallelism, either at the architecture or the algorithm level, is a significant departure from the traditional sequential approach. Languages and tools for parallel processing are designed to separate software development concerns from effective parallel execution concerns and provide both abstraction and standardization. To use parallel machines software, developers are required to first develop algorithms that are different than the ones they use on sequential machines and then to express their new algorithms using parallel languages or parallel extensions to existing languages. Parallel programming languages and environment should support the user in all phases of the parallel program development process.

For the development of communications software com- posed of many modules, protocol validation is essential to detect errors in the interactions among the modules. A number of protocol validation techniques were proposed in the past, but the validation time required by these techniques is too long for many actual protocols. This paper proposes a new fast protocol validation technique to overcome this drawback. The proposed technique is to construct the minimum acyclic form of state transitions in individual processes of the protocol, and to detect protocol errors such as system deadlocks and channel overflows fast. This paper also presents a protocol validation system based on the proposed technique to confirm its feasibility and shows validation results for some actual protocols obtained with this system. As a result, the protocol validation system is expected to contribute to a great extent to the improvement of the productivity in development and maintenance of communications software. [ABSTRACT FROM AUTHOR]

This paper presents an innovative model of a program's internal behavior over a set of test inputs, called the probabilistic program dependence graph (PPDG), which facilitates probabilistic analysis and reasoning about uncertain program behavior, particularly that associated with faults. The PPDG construction augments the structural dependences represented by a program dependence graph with estimates of statistical dependences between node states, which are computed from the test set. The PPDG is based on the established framework of probabilistic graphical models, which are used widely in a variety of applications. This paper presents algorithms for constructing PPDGs and applying them to fault diagnosis. The paper also presents preliminary evidence indicating that a PPDG-based fault localization technique compares favorably with existing techniques. The paper also presents evidence indicating that PPDGs can be useful for fault comprehension. [ABSTRACT FROM AUTHOR]

Search-based optimization techniques have been applied to structural software test data generation since 1992, with a recent upsurge in interest and activity within this area. However, despite the large number of recent studies on the applicability of different search-based optimization approaches, there has been very little theoretical analysis of the types of testing problem for which these techniques are well suited. There are also few empirical studies that present results for larger programs. This paper presents a theoretical exploration of the most widely studied approach, the global search technique embodied by Genetic Algorithms. It also presents results from a large empirical study that compares the behavior of both global and local search-based optimization on realworld programs. The results of this study reveal that cases exist of test data generation problem that suit each algorithm, thereby suggesting that a hybrid global-local search (a Memetic Algorithm) may be appropriate. The paper presents a Memetic Algorithm along with further empirical results studying its performance. [ABSTRACT FROM AUTHOR]

Abstract--Since modern software systems are large and complex, appropriate abstractions of their structure are needed to make them more understandable and. thus, easier to maintain. Software clustering techniques are useful to support the creation of these abstractions by producing architectural-level views of a system's structure directly from its source code. This paper examines the Bunch clustering system which, unlike other software clustering tools, uses search techniques to perform clustering. Bunch produces a subsystem decomposition by partitioning a graph of the entities (e.g.. classes) and relations (e.g., function calls) in the source code. Bunch uses a fitness function to evaluate the quality of graph partitions and uses search algorithms to find a satisfactory solution. This paper presents a case study to demonstrate how Bunch can be used to create views of the structure of significant software systems. This paper also outlines research to evaluate the software clustering results produced by Bunch. [ABSTRACT FROM AUTHOR]

Detecting strong conjunctive predicates is a fundamental problem in debugging and testing distributed programs. A strong conjunctive predicate is a logical statement to represent the desired event of the system. Therefore, if the predicate is not true, an error may occur because the desired event does not happen. Recently, several reported detection algorithms reveal the problem of unbounded state queue growth since the system may generate a huge amount of execution states in a very short time. In order to solve this problem. this paper introduces the notion of removable states which can be disregarded in the sense, that detection results still remain correct. A fully distributed algorithm is developed in this paper to perform the detection in an online manner. Based on the notion of removable states, the time complexity of the detection algorithm is improved as the number of states to be evaluated is reduced. [ABSTRACT FROM AUTHOR]

Regeneration with Virtual Copies is a voting-based consistency control algorithm for replicated data objects in a distributed computing system. Proposed by Adam and Tewari, it utilizes selective regeneration and recovery mechanisms for maintaining the availability and consistency of copies. This paper describes some problems with the original paper and proposes solutions. [ABSTRACT FROM AUTHOR]

Predicates appear in both the specification and implementation of a program. One approach to software testing, referred to as predicate testing, is to require certain types of tests for a predicate. In this paper, three fault-based testing criteria are defined for compound predicates, which are predicates with one or more AND/OR operators. BOR (boolean operator) testing requires a set of tests to guarantee the detection of (single or multiple) boolean operator faults, including incorrect AND/OR operators and missing/extra NOT operators. BRO (boolean and relational operator) testing requires a set of tests to guarantee the detection of boolean operator faults and relational operator faults (i.e., incorrect relational operators). BRE (boolean and relational expression) testing requires a set of tests to guarantee the detection of boolean operator faults, relational operator faults, and a type of fault involving arithmetical expressions. It is shown that for a compound predicate with n, n < 0, AND/OR operators, at most n + 2 constraints are needed for BOR testing and at most 2 * n + 3 constraints for BRO or BRE testing, where each constraint specifies a restriction on the value of each boolean variable or relational expression in the predicate. Algorithms for generating a minimum set of constraints for BOR, BRO, and BRE testing of a compound predicate are given, and the feasibility problem for the generated constraints is discussed. For boolean expressions that contain multiple occurrences of some boolean variables, how to combine BOR testing with the meaningful impact strategy developed by Weyuker, Goradia, and Singh [21] is briefly described. [ABSTRACT FROM AUTHOR]

There has been a recent rise in research on real-time problem solving algorithms in artificial intelligence (AI). A real-time AI problem solver performs a task or a set of tasks in two phases. During the first phase, the problem solver searches for a solution that, once executed, will satisfy the requirements of the task. We refer to this phase as the planning phase or the search phase. During the next phase, the problem solver executes the planned solution to achieve the desired results of the task. This phase is referred to as the execution phase. Under time constraints, a real-time AI problem solver must balance planning and execution to minimize total response times and to comply with deadlines. This paper provides a methodology for the specification of real-time AI problem solvers. Using this methodology, we provide a formal specification of a real-time problem. In addition, the paper presents a methodology for analyzing real-time AI problem solvers. This methodology is demonstrated via a case study of two real-time problem solvers, namely DYNORAII and RTA* [1], for the real-time path planning problem. We provide new results on worst-case and avenge-case complexity of the problem, and of the algorithms that solve it. We also provide experimental evaluation of DYNORAII and RTA* for deadline compliance and response-time minimization. [ABSTRACT FROM AUTHOR]

This paper treats the file redundancy issue in distributed database systems, asking what is the optimal number of rile copies, given the ratio r of the frequency of update requests to the frequency of all file access requests (i.e., queries and updates). Formulations of this type of problem, including optimal file allocation, have been attempted by a number of authors, and some algorithms have been proposed. Although such algorithms can be used to solve particular problems, it seems difficult to draw general conclusions applicable to a wide variety of practical distributed database systems. To probe into this hard to formulate but interesting problem, our paper constructs simplified network models of distributed database systems, and computes the optimal number of file copies, as well as their locations, to minimize the communication cost. For several network types, we plot the optimal number of rile copies as a function of the ratio r. Our conclusion is that a single copy suffices under most conditions, and it is disadvantageous to have more than a few copies unless the frequency of query requests is much higher (e.g., 50 times) than that of update requests. [ABSTRACT FROM AUTHOR]

In a distributed computing system made up of different types of processors each processor in the system may have different performance and reliability characteristics. In order to take advantage of this diversity of processing power, a modular distributed program should have its modules assigned in such a way that the applicable system performance index, such as execution time or cost, is optimized. This paper describes an algorithm for making an optimal module to processor assignment for a given performance criteria. We first propose a computational model to characterize distributed programs, consisting of tasks and an operational precedence relationship. This model allows us to describe probabilistic branching as well as concurrent execution in a distributed program. The computational model along with a set of seven program descriptors completely specifies a model for dynamic execution of a program on a distributed system. The optimal task to processor assignment is found by an algorithm based on results in Markov decision theory. The algorithm given in this paper is completely general and applicable to N-processor systems. [ABSTRACT FROM AUTHOR]

It is a staple development practice to log system behavior. Numerous powerful model-inference algorithms have been proposed to aid developers in log analysis and system understanding. Unfortunately, existing algorithms are typically declared procedurally, making them difficult to understand, extend, and compare. This paper presents InvariMint, an approach to specify model-inference algorithms declaratively. We applied the InvariMint declarative approach to two model-inference algorithms. The evaluation results illustrate that InvariMint (1) leads to new fundamental insights and better understanding of existing algorithms, (2) simplifies creation of new algorithms, including hybrids that combine or extend existing algorithms, and (3) makes it easy to compare and contrast previously published algorithms. InvariMint’s declarative approach can outperform procedural implementations. For example, on a log of 50,000 events, InvariMint’s declarative implementation of the kTails algorithm completes in 12 seconds, while a procedural implementation completes in 18 minutes. We also found that InvariMint’s declarative version of the Synoptic algorithm can be over 170 times faster than the procedural implementation. [ABSTRACT FROM PUBLISHER]

Model-based testing employs models for testing. Model-based mutation testing (MBMT) additionally involves fault models, called mutants, by applying mutation operators to the original model. A problem encountered with MBMT is the elimination of equivalent mutants and multiple mutants modeling the same faults. Another problem is the need to compare a mutant to the original model for test generation. This paper proposes an event-based approach to MBMT that is not fixed on single events and a single model but rather operates on sequences of events of length k ≥ 1 and invokes a sequence of models that are derived from the original one by varying its morphology based on k. The approach employs formal grammars, related mutation operators, and algorithms to generate test cases, enabling the following: (1) the exclusion of equivalent mutants and multiple mutants; (2) the generation of a test case in linear time to kill a selected mutant without comparing it to the original model; (3) the analysis of morphologically different models enabling the systematic generation of mutants, thereby extending the set of fault models studied in related literature. Three case studies validate the approach and analyze its characteristics in comparison to random testing and another MBMT approach. [ABSTRACT FROM PUBLISHER]

This article provides information about five articles selected from the Sixth International Workshop on Petri Nets and Performance Models, held in Durham, North Carolina, between October 3-6, 1995. Papers appearing in the workshop provides an excellent view of the recent research results on the theory and application of timed and stochastic Petri nets and related models. Papers are selected on the basis of their significance and have undergone a new, independent review process. The first of the five papers, titled, "Algorithms for the Generation of State-Level Representations of Stochastic Activity Networks With General Reward Structures," by M.A. Qureshi and colleagues, discusses the definition of stochastic activity networks, a variant of stochastic Petri nets, whose behavior is well specified. Stochastic Petri nets are often accused of being so natural for the description of complex behaviors that it is all too easy to come up with a correct model of a system, only to find out that its solution requires an excessive amount of resources. In another paper "Numerical Analysis of Superposed GSPNs," by researcher P. Kemper, presents an enhanced solution algorithm based on Kronecker algebra. A superposed generalized stochastic Petri Net (GSPN) is obtained when composing a set of subGSPNs by merging some transitions.

Slicing is useful for many software engineering applications and has been widely studied for three decades, but there has been comparatively little work on slicing extended finite state machines (EFSMs). This paper introduces a set of dependence-based EFSM slicing algorithms and an accompanying tool. We demonstrate that our algorithms are suitable for dependence-based slicing. We use our tool to conduct experiments on 10 EFSMs, including benchmarks and industrial EFSMs. Ours is the first empirical study of dependence-based program slicing for EFSMs. Compared to the only previously published dependence-based algorithm, our average slice is smaller 40 percent of the time and larger only 10 percent of the time, with an average slice size of 35 percent for termination insensitive slicing. [ABSTRACT FROM PUBLISHER]

In real-time systems, correctness depends not only on functionality but also on timeliness. A great number of scheduling theories have been developed for verification of the temporal correctness of jobs (software) in such systems. Among them, the Earliest Deadline first until Zero-Laxity (EDZL) scheduling algorithm has received growing attention thanks to its effectiveness in multicore real-time scheduling. However, the true potential of EDZL has not yet been fully exploited in its schedulability analysis as the state-of-the-art EDZL analysis techniques involve considerable pessimism. In this paper, we propose a new EDZL multicore schedulability test. We first introduce an interesting observation that suggests an insight toward pessimism reduction in the schedulability analysis of EDZL. We then incorporate it into a well-known existing Earliest Deadline First (EDF) schedulability test, resulting in a new EDZL schedulability test. We demonstrate that the proposed EDZL test not only has lower time complexity than existing EDZL schedulability tests, but also significantly improves the schedulability of EDZL by up to 36.6 percent compared to the best existing EDZL schedulability tests. [ABSTRACT FROM PUBLISHER]

This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), i.e., finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact--the resulting CFM precisely accepts the set of positive scenarios and rejects all negative ones--and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach. [ABSTRACT FROM AUTHOR]

This paper presents a technique that leverages an existing regression test selection algorithm to compute accurate, updated coverage data on a version of the software, Pi+1, without rerunning any test cases that do not execute the changes from the previous version of the software, Pi to Pi+1. The technique also reduces the cost of running those test cases that are selected by the regression test selection algorithm by performing a selective instrumentation that reduces the number of probes required to monitor the coverage data. Users of our technique can avoid the expense of rerunning the entire test suite on Pi+1 or the inaccuracy produced by previous approaches that estimate coverage data for Pi+1 or that reuse outdated coverage data from Pi. This paper also presents a tool, RECOVER, that implements our technique, along with a set of empirical studies on a set of subjects that includes several industrial programs, versions, and test cases. The studies show the inaccuracies that can exist when an application--regression test selection--uses estimated or outdated coverage data. The studies also show that the overhead incurred by selective instrumentation used in our technique is negligible and overall our technique provides savings over earlier techniques. [ABSTRACT FROM AUTHOR]

Providing evidence for the refutation of a property is an essential, if not the most important, feature of model checking. This paper considers algorithms for counterexample generation for probabilistic CTL formulas in discrete-time Markov chains. Finding the strongest evidence (i.e., the most probable path) violating a (bounded) until-formula is shown to be reducible to a single-source (hop-constrained) shortest path problem. Counterexamples of smallest size that deviate most from the required probability bound can be obtained by applying (small amendments to) k-shortest (hop-constrained) paths algorithms. These results can be extended to Markov chains with rewards, to LTL model checking, and are useful for Markov decision processes. Experimental results show that, typically, the size of a counterexample is excessive. To obtain much more compact representations, we present a simple algorithm to generate (minimal) regular expressions that can act as counterexamples. The feasibility of our approach is illustrated by means of two communication protocols: leader election in an anonymous ring network and the Crowds protocol. [ABSTRACT FROM AUTHOR]

Distributed systems often use a form of communication middleware to cope with different forms of heterogeneity, including geographical spreading of the components, different programming languages and platform architectures, etc. The middleware will, of course, impact the architecture and the performance of the system. This paper presents a model transformation framework to automatically include the architectural impact and the overhead incurred by using a middleware layer between several system components. Using this framework, architects can model the system in a middleware-independent fashion. Accurate, middleware- aware models can then be obtained automatically using a middleware model repository. The actual transformation algorithm will be presented in more detail. The resulting models can be used to obtain performance models of the system. From those performance models, early indications of the system performance can be extracted. [ABSTRACT FROM AUTHOR]

Software testing is particularly expensive for developers of high-assurance software, such as software that is produced for commercial airborne systems. One reason for this expense is the Federal Aviation Administration's requirement that test suites be modified condition/decision coverage (MC/DC) adequate. Despite its cost, there is evidence that MC/DC is an effective verification technique and can help to uncover safety faults. As the software is modified and new test cases are added to the test suite, the test suite grows and the cost of regression testing increases. To address the test-suite size problem, researchers have investigated the use of test-suite reduction algorithms, which identify a reduced test suite that provides the same coverage of the software according to some criterion as the original test suite, and test-suite prioritization algorithms, which identify an ordering of the test cases in the test suite according to some criteria or goals. Existing test-suite reduction and prioritization techniques, however, may not be effective in reducing or prioritizing MC/DC-adequate test suites because they do not consider the complexity of the criterion. This paper presents new algorithms for test-suite reduction and prioritization that can be tailored effectively for use with MC/DC. The paper also presents the results of empirical studies of these algorithms. [ABSTRACT FROM AUTHOR]

We report an error in a verification model in [41 and present a revised model with verification result. Our result explains the reason why SPIN found the race condition in the synchronization algorithm. We also show that the suggested fix in [4] is incorrect. [ABSTRACT FROM AUTHOR]

Formal techniques for the specification of real-time systems must be capable of describing system behavior as a set of relationships expressing the temporal constraints among events and actions, including properties of invariance, precedence, periodicity, liveness, and safety conditions. This paper describes a Temporal-Interval Logic with Compositional Operators (TILCO) designed expressly for the specification of real-time systems. TILCO is a generalization of classical temporal logics based on the operators eventually and henceforth; it allows both qualitative and quantitative specification of time relationships. TILCO is based on time intervals and can concisely express temporal constraints with time bounds, such as those needed to specify real-time systems. This approach can be used to verify the completeness and consistency of specifications, as well as to validate system behavior against its requirements and general properties. TILCO has been formalized by using the theorem prover Isabelle/HOL. TILCO specifications satisfying certain properties are executable by using a modified version of the Tableaux algorithm. This paper defines TILCO and its axiomatization, highlights the tools available for proving properties of specifications and for their execution, and provides an example of system specification and validation. [ABSTRACT FROM AUTHOR]

Distributed application systems are composed of classes of objects with instances that interact to accomplish common goals. Such systems can have many classes of users with many types of requests. Furthermore, the relative load of these classes can shift throughout the day causing changes to system behavior and bottlenecks. When designing and deploying such systems it is necessary to determine a process replication and threading policy for the server processes that contain the objects, as well as process activation policies. To avoid bottlenecks the policy must support all possible workload conditions Licensing, implementation, or resource constraints can limit the number of permitted replicas or threads of a server process Process activation policies determine whether a server is persistent or should be created and terminated with each call. The purpose of this paper is to describe quantitative techniques for choosing process replication or threading levels and process activation policies. Inappropriate policies can lead to unnecessary queuing delays for callers or unnecessarily high consumption of memory resources. The algorithms presented consider all workload conditions, are iterative in nature, and are hybrid mathematical programming and analytic performance evaluation methods. An example is given to demonstrate the technique and describe how the results can be applied during software design and deployment. [ABSTRACT FROM AUTHOR]

Global predicate detection is a fundamental problem in distributed systems and finds applications in many domains such as testing and debugging distributed programs. This paper presents an efficient distributed algorithm to detect conjunctive form global predicates in distributed systems. The algorithm detects the first consistent global state that satisfies the predicate even if the predicate is unstable. Unlike previously proposed run-time predicate detection algorithms, our algorithm does not require exchange of control messages during the normal computation. All the necessary information to detect predicates is piggybacked on computation messages of application programs. The algorithm is distributed because the predicate detection efforts as well as the necessary information are equally distributed among the processes. We prove the correctness of the algorithm and compare its performance with respect to message, storage, and computational complexities with that of the previously proposed run-time predicate detection algorithms. [ABSTRACT FROM AUTHOR]

This paper addresses the problem of jointly scheduling tasks with both hard and soft real-time constraints. We present a new analysis applicable to systems scheduled using a priority preemptive dispatcher, with priorities assigned dynamically according to the EDF policy. Further, we present a new efficient on-line algorithm (the acceptor algorithm) for servicing aperiodic work load. The acceptor transforms a soft aperiodic task into a hard one by assigning a deadline. Once transformed, aperiodic tasks are handled in exactly the same way as periodic tasks with hard deadlines. The proposed algorithm is shown to be optimal in terms of providing the shortest aperiodic response time among fixed- and dynamic-priority schedulers. It always guarantees the proper execution of periodic hard tasks. The approach is composed of two parts: an off-line analysis and a run-time scheduler. The off-line algorithm runs in pseudopolynomial time O(mn), where n is the number of hard periodic tasks and m is the hyperperiod/min deadline. [ABSTRACT FROM AUTHOR]

Stochastic Petri net models of large systems that are solved by generating the underlying Markov chain pose the problem of largeness of the state-space of the Markov chain. Hierarchical and iterative models of systems have been used extensively to solve this problem. A problem with models which use fixed-point iteration is the theoretical proof of existence, uniqueness, and convergence of the fixed-point equations, which still remains an "art." In this paper, we establish conditions, in ternis of the net structure and the characteristics of the iterated variables, under which existence of a solution is guaranteed when fixed-point iteration is used in stochastic Petri nets. We use these conditions to establish the existence of a fixed point for a model of a priority scheduling system, at which tasks may arrive according to a Poisson process or due to spawning or conditional branching of other tasks in the system. [ABSTRACT FROM AUTHOR]

Interprocedural data flow information is useful for many software testing and analysis techniques, including data flow testing, regression testing, program slicing, and impact analysis. For programs with aliases, these testing and analysis techniques can yield invalid results, unless the data flow information accounts for aliasing effects. Recent research provides algorithms for performing interprocedural data flow analysis in the presence of aliases; however, these algorithms are expensive, and achieve precise results only on complete programs. This paper presents an algorithm for performing alias analysis on incomplete programs that lets individual software components such as library routines, subroutines, or subsystems be independently analyzed. The paper also presents an algorithm for reusing the results of this separate analysis when the individual software components are linked with calling modules. Our algorithms let us analyze frequently used software components, such as library routines or classes, independently, and reuse the results of that analysis when analyzing calling programs, without incurring the expense of completely reanalyzing each calling program. Our algorithms also provide a way to analyze large systems incrementally. [ABSTRACT FROM AUTHOR]

Scheduling theory holds gnat promise as a means to a priori validate timing correctness of real-time applications. However, there currently exists a wide gap between scheduling theory and its implementation in operating system kernels running on specific hardware platforms. The implementation of any particular scheduling algorithm introduces overhead and blocking components which must be accounted for in the timing correctness validation process. This paper presents a methodology for incorporating the costs of scheduler implementation within the context of fixed priority scheduling algorithms. Both event-driven and timer-driven scheduling implementations are analyzed. We show that for the timer-driven scheduling implementations the selection of the timer interrupt rate can dramatically affect the schedulability of a task set, and we present a method for determining the optimal timer rate. We analyzed both randomly generated and two well-defined task sets and found that their schedulability can be significantly degraded by the implementation costs. Task sets that have ideal breakdown utilization over 90% may not even be schedulable when the implementation costs are considered. This work provides a first step toward bridging the gap between real-time scheduling theory and implementation realities. This gap must be bridged for any meaningful validation of timing correctness properties of real- time applications. [ABSTRACT FROM AUTHOR]

L.0 is a programming language designed for the specification and simulation of protocols. The model of concurrency assumed in L.0 is a true concurrency model, rather than an interleaving semantics model. Thus, simultaneous occurrence of events may be easily specified in L.0. This paper gives the semantics of L.0 in terms of predicate linear temporal logic and defines the restricted universe of models assumed in L.0 programs. The execution algorithm for L.0 constructs a model in this universe. The restricted subset of temporal logic exploited permits a nonbacktracking execution algorithm. Fundamental to the semantics of L.0 is a frame assumption, which generalizes the frame assumption of standard imperative programming, and which eases specification of protocols. The data domain assumed in L.0 programs is sets of trees with labeled edges, and the state predicates permitted include existence and nonexistence predicates, as well as the more traditional assignment and equality predicates. These choices for data domain and predicates permit convenient specification of the hierarchical message structure often assumed in telecommunications protocols. For in such message structures, the existence or nonexistence of parts of the message hierarchy is determined by logical properties of the rest of the message hierarchy. The subject of the main example in the paper is a small portion of the Logical Layer Specification of Futurebus+. [ABSTRACT FROM AUTHOR]

Resource allocation problems for distributed systems have been extensively studied for years. However, not many studies consider failure/repair behaviors of the systems and fault- tolerant overhead. As a result, solutions may not be applicable to fault-tolerant systems. In this paper, we study resource allocation for a distributed system employing the primary site approach for fault tolerance. Two kinds of systems are considered in this paper. The first consists of fault-tolerant nodes where each node has many duplicated servers. One server is the primary, which serves user requests, and the rest are backup. The second does not have fault-tolerant nodes. To tolerate node failures, each node uses other nodes as backups. When a node fails, all requests initially allocated to the node are served by one of its backups. To study the resource allocation for such systems, we develop an approximate model for each system. With these models, efficient allocation algorithms are presented, which takes into account the failure/repair rates of the system and the fault-tolerant overheads. From many experiments, it is shown that the algorithms give the optimal or suboptimal allocations. The algorithms, which incur little overhead, can improve the system performance significantly over an intuitive allocation algorithm. [ABSTRACT FROM AUTHOR]

This paper describes a proof system suitable for the mechanical verification of concurrent programs. Mechanical verification, which uses a computer program to validate a formal proof, increases one's confidence in the correctness of the validated proof. This proof system is based on Unity [12], and may be used to specify and verify both safety and liveness properties. However, it is defined with respect to an operational semantics of the transition system model of concurrency. Proof rules are simply theorems of this operational semantics. This methodology makes a clear distinction between the theorems in the proof system and the logical inference rules and syntax which define the underlying logic. Since this proof system essentially encodes Unity in another sound logic, and this encoding has been mechanically verified, this encoding proves the soundness of this formalization of Unity. This proof system has been mechanically verified by the Boyer-Moore prover, a computer program mechanizing the Boyer-Moore logic [7]. This proof system has been used to mechanically verify the correctness of a distributed algorithm that computes the minimum node value in a tree. This paper also describes this algorithm and its correctness theorems, and presents the key lemmas that aided the mechanical verification. The mechanized proof closely resembles a hand proof, but is longer, since all concepts are defined from first principles. This proof system is suitable for the mechanical verification of a wide class of programs, since the underlying prover, though automatic, is guided by the user. [ABSTRACT FROM AUTHOR]

A new approach to coordination of cooperating concurrent processes, each capable of error detection and recovery, is presented. Error detection, rollback, and retry in a process are specified by a well-structured language construct called recovery block. Recovery points of processes must be properly coordinated to prevent a disastrous avalanche of process rollbacks. In contrast to the previously studied approaches that require the program designer to coordinate the recovery block structures of interacting processes (thereby coordinating the recovery points of processes), the new approach relieves the program designer of that burden It instead relies upon an intelligent processor system (that runs processes) capable of establishing and discarding the recovery points of interacting processes in a well coordinated manner such that 1) a process never makes two consecutive rollbacks without making a retry between the two, and 2) every process rollback becomes a minimum-distance rollback. Following the discussion of the underlying philosophy of the new approach, basic rules of reducing storage and time overhead in such a processor system are discussed. Throughout this paper examples are drawn from the systems in which processes communicate through monitors. [ABSTRACT FROM AUTHOR]

A modification of the linear quadtree [3], the threaded linear hierarchical quadtree (TLHQT), is proposed for the computation of geometric properties of binary images. Since most of the algorithms used in connection with computation of geometric properties require frequent exploration of adjacencies, a structure which keeps permanently in memory some adjacency links is introduced. In this paper, we present some results obtained by using the TLHQT for labeling connected components, evaluating perimeter and Euler's number in a quadtree environment. The algorithms for computing perimeter and Euler number and the first phase of the labeling algorithm are shown to have time complexity O(B), where B is the number of black nodes of the quadtree. The authors determine the adjacency links at the very beginning—namely, when the binary image is mapped from raster scan to the quadtree. Pixel adjacency is, in fact, available during row scanning, and node's adjacency is easy to evaluate locally when performing condensation of nodes into larger quadrants and also while merging partial quadtrees. Although the structure requires space nearly four times as much as the linear quadtree, the requirement is roughly half that for the pointer-based quadtree. Also it appears that for computing geometric properties, the TLHQT offers execution timings better than those obtained by both the linear and pointer-based quadtrees and the graph structure reported in [16]. [ABSTRACT FROM AUTHOR]

In recent years there has been a tremendous spurt in re- search and activity in finding efficient compression techniques for image processing applications. Particularly when an image is structured over a nonrectangular region, it is always advantageous to define a method of covering a region by minimal numbers of maximal rectangles. Towards this objective, we analyze the binary image compression problem using irreducible cover of maximal rectangles. We also give a hound on the minimum rectangular cover problem for image compression under certain conditions that previously have not been analyzed. It is demonstrated that for a simply connected image, the irreducible cover proposed here uses less than four times the number of the rectangles in a minimum cover. With n pixels in a square, the parallel algorithm of obtaining the irreducible cover presented in the paper uses (n/log n) concurrent-read-exclusive-write (CREW) processors in O( log n) time. [ABSTRACT FROM AUTHOR]

Distributed database systems (DUBS) have received considerable attention in recent years. Being a relatively young research field, there are still many problems associated with DDB systems that need solution. Concurrency control is one of these problems and, probably, the most extensively studied. However, most of the work has concentrated on the development of alternative solutions and the field seems to be ready for some comparative analysis work. This paper reports the results of a performance evaluation study on distributed database concurrency control algorithms. The research has resulted in the development of a formalism, based on Petri nets, for modeling and analysis purposes. The formalism, called the Extended Place/Transition Nets (EPTN), is both descriptively powerful in that it can be used to model various algorithms precisely and succinctly and to communicate them in a clear manner, while at the same time lending itself to be used as a performance evaluation tool. An EPTN simulator is implemented and various algorithms are studied using this tool. This paper describes both the formalism and the performance results that have been obtained. [ABSTRACT FROM AUTHOR]

It is desirable for the load in a distributed system to be balanced evenly. A dynamic process migration protocol is needed in order to achieve load balancing in a user transparent manner. A distributed algorithm for load balancing which is network topology independent is proposed in this paper. Different network topologies and low-level communications protocols affect the choice of only some system design parameters. The "drafting" algorithm attempts to compromise two contradictory goals: maximize the processor utilization and minimize the communication overhead. The main objective of this paper is to describe the dynamic process migration protocol based on the proposed drafting algorithm. A sample distributed system is used to further illustrate the drafting algorithm and to show how to define system design parameters. The system performance is measured by simulation experiments based on the sample system. [ABSTRACT FROM AUTHOR]

This paper proposes a model or paradigm for the development of parallel algorithms, gives an example of the proposed paradigm, and displays algorithms developed by application of the technique. The algorithm for the merge of two ordered fists developed through application of this technique is thought to be original. The paradigm proposed is to create composite unit operations which combine data movement between data structures with a conventional operation such as compare or add. The composite operation constructed for this study is based upon partitioning the data elements into two linear lists. Exchange of data between adjacent elements in each list are then combined with compares and adds to complete the composite operations. This composite operation can be implemented on at least the following computational architectures. 1) SIMD with all processors sharing a common memory. 2) SIMD with local memories and a linear interconnection (circular pipeline or ring network of processors). 3) Vector processor with common memory, such as a CDC CYBER 205 or a Cray Research CRAY-1. The algorithms developed all have the property of linear speed-up with the number of processing elements. The algorithms developed include sorting, merging, selection among sets, set interconnection, set difference, subset testing, and string matching. [ABSTRACT FROM AUTHOR]

As multiple processor systems become more widely accepted the importance of parallel programming increases. In this paper, approaches to the design and analysis of parallel algorithms are investigated. Through several examples, the importance of interprocessor communication in parallel processing is demonstrated. Various techniques that are applicable in the design and analysis of parallel algorithms are examined with emphasis on those techniques that incorporate communication aspects. The paper discusses several models of synchronous and asynchronous parallel computation and their use in analyzing algorithms. Relatively primitive methodologies for designing parallel algorithms are discussed and the need for more general and practical methodologies is indicated. [ABSTRACT FROM AUTHOR]

Software maintenance is the dominant factor contributing to the high cost of software. In this paper, the software maintenance process and the important software quality attributes that affect the maintenance effort are discussed. One of the most important quality attributes of software maintainability is the stability of a program, which indicates the resistance to the potential ripple effect that the program would have when it is modified. Measures for estimating the stability of a program and the modules of which the program is composed are presented. and an algorithm for computing these stability measures is given. An algorithm for normalizing these measures is also given. Applications of these measures during the maintenance phase are discussed along with an example. An indirect validation of these stability measures is also given. Future research efforts involving application of these measures during the design phase, program restructuring based on those measures, and the development of an overall maintainability measure arc also discussed. [ABSTRACT FROM AUTHOR]

This paper contains algorithms for ensuring the consistency of a distributed relational data base subject to multiple, concurrent updates. Also included are mechanisms to correctly update multiple copies of objects and to continue operation when less than all machines in the network are operational. Together with [4] and [12], this paper constitutes the significant portions of the design for a distributed data base version of INGRES. [ABSTRACT FROM AUTHOR]

As the complexity of model transformations grows, there is an increasing need to count on methods, mechanisms, and tools for checking their correctness, i.e., the alignment between specifications and implementations. In this paper we present a light-weight and static approach for locating the faulty rules in model transformations, based on matching functions that automatically establish these alignments using the metamodel footprints, i.e., the metamodel elements used. The approach is implemented for the combination of Tracts and ATL, both residing in the Eclipse Modeling Framework, and is supported by the corresponding toolkit. An evaluation discussing the accuracy and the limitations of the approach is also provided. Furthermore, we identify the kinds of transformations which are most suitable for validation with the proposed approach and use mutation techniques to evaluate its effectiveness. [ABSTRACT FROM PUBLISHER]

Decision-based processes are composed of tasks whose application may depend on explicit decisions relying on the state of the process environment. In specific domains such as healthcare, decision-based processes are often complex and critical in terms of timing and resources. The paper presents a variety of tool-supported techniques for analyzing models of such processes. The analyses allow a variety of errors to be detected early and incrementally on partial models, notably: inadequate decisions resulting from inaccurate or outdated information about the environment state; incomplete decisions; non-deterministic task selections; unreachable tasks along process paths; and violations of non-functional process requirements involving time, resources or costs. The proposed techniques are based on different instantiations of the same generic algorithm that propagates decorations iteratively through the process model. This algorithm in particular allows event-based models to be automatically decorated with state-based invariants. A formal language supporting both event-based and state-based specifications is introduced as a process modeling language to enable such analyses. This language mimics the informal flowcharts commonly used by process stakeholders. It extends High-Level Message Sequence Charts with guards on task-related and environment-related variables. The language provides constructs for specifying task compositions, task refinements, decision trees, multi-agent communication scenarios, and time and resource constraints. The proposed techniques are demonstrated on the incremental building and analysis of a complex model of a real protocol for cancer therapy. [ABSTRACT FROM PUBLISHER]

We present Magiclock, a novel potential deadlock detection technique by analyzing execution traces (containing no deadlock occurrence) of large-scale multithreaded programs. Magiclock iteratively eliminates removable lock dependencies before potential deadlock localization. It divides lock dependencies into thread specific partitions, consolidates equivalent lock dependencies, and searches over the set of lock dependency chains without the need to examine any duplicated permutations of the same lock dependency chains. We validate Magiclock through a suite of real-world, large-scale multithreaded programs. The experimental results show that Magiclock is significantly more scalable and efficient than existing dynamic detectors in analyzing and detecting potential deadlocks in execution traces of large-scale multithreaded programs. [ABSTRACT FROM PUBLISHER]

The above paper' proposes a distributed query optimization algorithm called GENERAL. Lakhani and Wang [4] point out that the results obtained by the algorithm are not optimal. In this correspondence we point out another erroneous fact concerning the assumption of irreducibility of nonjoining attributes. We show that it is possible to generate an efficient semijoin programs with better response time than the one produced by the GENERAL algorithm. [ABSTRACT FROM AUTHOR]

Synthesis of operational behavior models from scenario-based specifications has been extensively studied. The focus has been mainly on either existential or universal interpretations. One noteworthy exception is Live Sequence Charts (LSCs), which provides expressive constructs for conditional universal scenarios and some limited support for nonconditional existential scenarios. In this paper, we propose a scenario-based language that supports both existential and universal interpretations for conditional scenarios. Existing model synthesis techniques use traditional two-valued behavior models, such as Labeled Transition Systems. These are not sufficiently expressive to accommodate specification languages with both existential and universal scenarios. We therefore shift the target of synthesis to Modal Transition Systems (MTS), an extension of labeled Transition Systems that can distinguish between required, unknown, and proscribed behavior to capture the semantics of existential and universal scenarios. Modal Transition Systems support elaboration of behavior models through refinement, which complements an incremental elicitation process suitable for specifying behavior with scenario-based notations. The synthesis algorithm that we define constructs a Modal Transition System that uses refinement to characterize all the Labeled Transition Systems models that satisfy a mixed, conditional existential and universal scenario-based specification. We show how this combination of scenario language, synthesis, and Modal Transition Systems supports behavior model elaboration. [ABSTRACT FROM PUBLISHER]

The injection of software faults in software components to assess the impact of these faults on other components or on the system as a whole, allowing the evaluation of fault tolerance, is relatively new compared to decades of research on hardware fault injection. This paper presents an extensive experimental study (more than 3.8 million individual experiments in three real systems) to evaluate the representativeness of faults injected by a state-of-the-art approach (G-SWFIT). Results show that a significant share (up to 72 percent) of injected faults cannot be considered representative of residual software faults as they are consistently detected by regression tests, and that the representativeness of injected faults is affected by the fault location within the system, resulting in different distributions of representative/nonrepresentative faults across files and functions. Therefore, we propose a new approach to refine the faultload by removing faults that are not representative of residual software faults. This filtering is essential to assure meaningful results and to reduce the cost (in terms of number of faults) of software fault injection campaigns in complex software. The proposed approach is based on classification algorithms, is fully automatic, and can be used for improving fault representativeness of existing software fault injection approaches. [ABSTRACT FROM AUTHOR]

Web script crashes and malformed dynamically generated webpages are common errors, and they seriously impact the usability of Web applications. Current tools for webpage validation cannot handle the dynamically generated pages that are ubiquitous on today's Internet. We present a dynamic test generation technique for the domain of dynamic Web applications. The technique utilizes both combined concrete and symbolic execution and explicit-state model checking. The technique generates tests automatically, runs the tests capturing logical constraints on inputs, and minimizes the conditions on the inputs to failing tests so that the resulting bug reports are small and useful in finding and fixing the underlying faults. Our tool Apollo implements the technique for the PHP programming language. Apollo generates test inputs for a Web application, monitors the application for crashes, and validates that the output conforms to the HTML specification. This paper presents Apollo's algorithms and implementation, and an experimental evaluation that revealed 673 faults in six PHP Web applications. [ABSTRACT FROM AUTHOR]