Given a program P , one can construct a Kripke structure \(\mathcal{M}\) . Model checking verifies that P satisfies a behavioral property given by a temporal logic formula \(\varphi\) by checking that \(\mathcal{M}\) models \(\varphi\) . However, \(\mathcal{M}\) can be exponentially large in P . The action of a symmetry group G on \(\mathcal{M}\) and \(\varphi\) can produce a smaller structure \(\overline{\mathcal{M}}\) . When \(\mathcal{M}\) does not satisfy \(\varphi\) , one can look for a substructure that satisfies \(\varphi\) . We call this substructure repair . We show that repairs of \(\overline{\mathcal{M}}\) lift to repairs of \(\mathcal{M}\) , i.e., we can repair a concurrent program by repairing the smaller structure \(\overline{\mathcal{M}}\) and symmetrizing the resulting program. The substructures of \(\overline{\mathcal{M}}\) map to substructures of \(\mathcal{M}\) preserved by G . We present relative completeness results, which give conditions under which the existence of a repair of \(\mathcal{M}\) implies the existence of a repair of \(\overline{\mathcal{M}}\) . In cases where there is no repair of a Kripke structure \(\mathcal{M}\) w.r.t. a formula, we show that there are instances where it is possible to “unwind” \(\mathcal{M}\) to generate a structure \(\mathcal{M^{\prime}}\) that is strongly bisimilar to \(\mathcal{M}\) and for which a repair exists. This leads to a natural semantic notion, repairability , which is not preserved by strong bisimulation. We illustrate the combined use of symmetry reduction and unwinding to effect a repair. Finally, we provide closed-form results for the reductions in number of states in the Kripke structure that can be achieved by symmetry reduction.

Abstract Given a textual representation of a finite-state concurrent program $$P$$ P , one can construct the corresponding Kripke structure $$\mathcal {M}$$ M . However, the size of $$\mathcal {M}$$ M can be exponentially larger than the textual size of $$P$$ P . This state explosion can make model checking properties of $$P$$ P via $$\mathcal {M}$$ M expensive or even infeasible. The action of a symmetry group $$G$$ G on $$\mathcal {M}$$ M can be used to produce a smaller Kripke structure $$\overline{\mathcal {M}}$$ M ¯ . Various authors have exploited the direct correspondence between $$\mathcal {M}$$ M and $$\overline{\mathcal {M}}$$ M ¯ to perform model checking. When the structure $$\mathcal {M}$$ M does not satisfy a formula, one can look for a substructure that will satisfy the formula. We call this substructure-repair : identifying a substructure $$\mathcal {N}$$ N of $$\mathcal {M}$$ M that satisfies a given temporal logic formula. In this paper we extend previous work by showing that repairs of $$\overline{\mathcal {M}}$$ M ¯ lift to repairs of $$\mathcal {M}$$ M . In other words, we can repair a computer program $$P$$ P , which exhibits a high degree of symmetry, by repairing the smaller Kripke structure $$\overline{\mathcal {M}}$$ M ¯ and then symmetrizing the corresponding program. To do this we arrange the substructures of $$\mathcal {M}$$ M and $$\overline{\mathcal {M}}$$

We consider the subtractive model repair problem : given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M ′ that satisfies η. Thus, M can be “repaired” to satisfy eta by deleting some transitions and states. We map an instance 〈 M ,η 〉 of model repair to a Boolean formula repair ( M ,η) such that 〈 M ,η 〉 has a solution iff repair ( M ,η) is satisfiable. Furthermore, a satisfying assignment determines which states and transitions must be removed from M to yield a model M ′ of η Thus, we can use any SAT solver to repair Kripke structures. Using a complete SAT solver yields a complete algorithm: it always finds a repair if one exists. We also show that CTL model repair is NP-complete. We extend the basic repair method in three directions: (1) the use of abstraction mappings, that is, repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M , (2) repair concurrent Kripke structures and concurrent programs: we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program, as a set of “concurrent Kripke structures”, with only a quadratic increase in the size of the repair formula, and (3) repair hierarchical Kripke structures: we use a CTL formula to summarize the behavior of each “box,” and CTL deduction to relate the box formula with the overall specification.

We present a criterion for checking local and global deadlock freedom of finite state systems expressed in BIP: a component-based framework for constructing complex distributed systems. Our criterion is evaluated by model-checking a set of subsystems of the overall large system. If satisfied in small subsystems, it implies deadlock-freedom of the overall system. If not satisfied, then we re-evaluate over larger subsystems, which improves the accuracy of the check. When the subsystem being checked becomes the entire system, our criterion becomes complete for deadlock-freedom. Hence our criterion only fails to decide deadlock freedom because of computational limitations: state-space explosion sets in when the subsystems become too large. Our method thus combines the possibility of fast response together with theoretical completeness. Other criteria for deadlock freedom, in contrast, are incomplete in principle, and so may fail to decide deadlock freedom even if unlimited computational resources are available. Also, our criterion certifies freedom from local deadlock, in which a subsystem is deadlocked while the rest of the system executes. Other criteria only certify freedom from global deadlock. We present experimental results for dining philosophers and for a multi-token-based resource allocation system, which subsumes several data arbiters and schedulers, including Milner’s token-based scheduler.

Abstract Architectures depict design principles: paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They provide means for ensuring correctness by construction by enforcing global properties characterizing the coordination between components. An architecture can be considered as an operator A that, applied to a set of components B , builds a composite component A ( B ) meeting a characteristic property Φ . Architecture composability is a basic and common problem faced by system designers. In this paper, we propose a formal and general framework for architecture composability based on an associative, commutative and idempotent architecture composition operator ⊕ . The main result is that if two architectures A 1 and A 2 enforce respectively safety properties Φ 1 and Φ 2 , the architecture A 1 ⊕ A 2 enforces the property Φ 1 ∧ Φ 2 , that is both properties are preserved by architecture composition. We also establish preservation of liveness properties by architecture composition. The presented results are illustrated by a running example and a case study.

We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a reduction to boolean satisfiability, and implement the repair method using this reduction. We also extend the basic repair method in three directions: (1) the use of abstraction, and (2) the repair of concurrent Kripke structures and concurrent programs, and (3) the repair of hierarchical Kripke structures. These last two extensions both avoid state-explosion.

We prove two theorems saying that no distributed system in which processes coordinate using reliable registers and f-resilient services can solve the consensus problem in the presence of f + 1 undetectable process stopping failures. (A service is f-resilient if it is guaranteed to operate as long as no more than f of the processes connected to it fail.) Our first theorem assumes that the given services are atomic objects, and allows any connection pattern between processes and services. In contrast, we show that it is possible to boost the resilience of systems solving problems easier than consensus: the k-set consensus problem is solvable for 2k - 1 failures using 1-resilient consensus services. The first theorem and its proof generalize to the larger class of failure-oblivious services. Our second theorem allows the system to contain failure-aware services, such as failure detectors, in addition to failure-oblivious services; however, it requires that each failure-aware service be connected to all processes. Thus, f + 1 process failures overall can disable all the failure-aware services. In contrast, it is possible to boost the resilience of a system solving consensus if arbitrary patterns of connectivity are allowed between processes and failure-aware services: consensus is solvable for any number of failures using only 1-resilient 2-process perfect failure detectors

Methods for mechanically synthesizing concurrent programs from temporal logic specifications obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of extant synthesis methods, however, is that they produce concurrent programs for models of computation that are often unrealistic. In particular, these methods assume completely fault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we show how to mechanically synthesize fault-tolerant concurrent programs for various fault classes. We illustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barrier synchronization problems.

We introduce an alternative approach to congestion avoidance and control, which has the potential to increase efficiency and fairness in multiplexed channels. Our approach, bimodal congestion avoidance and control, is based on the principles of TCP's additive increase multiplicative decrease. It is designed to better exploit the system properties during equilibrium, without trading off responsiveness for smoothness. In addition, it is capable of achieving convergence to fairness in only two congestion cycles. As a result, both efficiency and fairness are improved, responsiveness is not degraded, and smoothness is significantly improved when the system is in equilibrium. We provide a theoretical analysis and we discuss the potential of our approach for packet networks. Our experiments confirm that bimodal congestion avoidance and control as a component of the transmission control protocol outperforms the traditional scheme.

We present a mathematical state-machine model, the Dynamic I/O Automaton (DIOA) model, for defining and analyzing dynamic systems of interacting components. The systems we consider are dynamic in two senses: (1) components can be created and destroyed as computation proceeds, and (2) the set of events in which a component may participate can change as computation proceeds. The new model admits a notion of external system behavior, based on sets of traces. It also features a parallel composition operator for dynamic systems, which satisfies standard execution projection and pasting results, and a notion of simulation from one dynamic system to another, which can be used to prove that one system implements the other.

Methods for mechanically synthesizing concurrent programs for temporal logic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (Manna and Wolper), processes with global information about the system state (Emerson and Clarke), or reactive modules that can read all of their inputs in one atomic step (Anuchitanukul and Manna, and Pnueli and Rosner). Even simple synchronization protocols based on atomic read/write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods. In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems. We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem.

We present a simulation-baaed proof method for live-neSs properties.Our method is based on simulation relations [8] that relate the liveness properties of an implementation to those of the specification.Even though reasoning about liveness is usually associated with reasoning over entire executions, variant functions, fairness etc., our method requires reasoning over individual states/transitions only.It thus presents a significant methodological advance over current methods.

Methods for mechanically synthesizing concurrent programs from temporal logic specificationsobviate the need to manually construct a program and compose a proof of its correctness. A seriousdrawback of extant synthesis methods, however, is that they produce concurrent programs formodels of computation that are often unrealistic. In particular, these methods assume completelyfault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we showhow to mechanically synthesize fault-tolerant concurrent programs for various fault classes. Weillustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barriersynchronization problems.Categories and Subject Descriptors: C.2.4 [

Methods for synthesizing concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. To synthesize a concurrent system consisting of K sequential processes, each having N states in its local transition diagram, requires construction of the global product-machine having about N K global states in general. This exponential growth in K makes it infeasible to synthesize systems composed of more than 2 or 3 processes. In this article, we show how to synthesize concurrent systems consisting of many (i.e., a finite but arbitrarily large number K of) similar sequential processes. Our approach avoids construction of the global product-machine for K processes; instead, it constructs a two-process product-machine for a single pair of generic sequential processes. The method is uniform in K , providing a simple template that can be instantiated for each process to yield a solution for any fixed K . The method is also illustrated on synchronization problems from the literature.

We present a new algorithm for detecting generalized deadlocks in distributed systems. Our algorithm incrementally constructs and reduces a wait-for graph (WFG) at an initiator process. This WFG is then searched for deadlock. The proposed algorithm has two primary advantages: First, it avoids sending messages along the edges of the global wait-for graph (WFG), thereby achieving a worst-case message complexity of 2n, where n is the number of processes in the WFG. Since information must be obtained from every process reachable from the initiator, this is optimal to within a constant factor. All the existing algorithms for the same problem construct a distributed snapshot of the WFG. As this involves sending messages along the edges of the WFG, the best available message complexity among these algorithms is 4e-2n+2l, which is O(n/sup 2/) in the worst case, where e and l are the number of edges and leaves in the WFG, respectively. Second, since the information about a detected deadlock is readily available at the initiator process, rather than distributed among different processes, it significantly simplifies the task of deadlock resolution, and helps to reduce system overhead associated with the resolution. The time complexity of our algorithm is also better than or equal to the existing algorithms.

Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed (cf.[EC82, MW84, PR$9, PR89b, AM94]).An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose a proof of its correctness.A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (cf.[MW84] ) or processes with global information about the system state (cf.[EC82]).Even simple synchronization protocols based on atomic read / atomic write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods.In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems.We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem.

The Carnot Project at MCC is addressing the problem of logically unifying physically-distributed, enterprise-wide, heterogeneous information. Carnot will provide a user with the means to navigate information efficiently and transparently, to update that information consistently, and to write applications easily for large, heterogeneous, distributed information systems. A prototype has been implemented which provides services for (a) enterprise modeling and model integration to create an enterprise-wide view, (b) semantic expansion of queries on the view to queries on individual resources, and (c) inter-resource consistency management. This paper describes the Carnot approach to transaction processing in environments where heterogeneous, distributed, and autonomous systems are required to coordinate the update of the local information under their control. In this approach, subtransactions are represented as a set of tasks and a set of intertask dependencies that capture the semantics of a particular relaxed transaction model. A scheduler has been implemented which schedules the execution of these tasks in the Carnot environment so that all intertask dependencies are satisfied.

A fairness property, called U-fairness, is studied in the context of the design of distributed systems with multiparty interactions. This is done with an overlapping model of concurrency. A distributed algorithm implementing the fairness notion is presented. U-fairness is shown to be more appropriate to the design of distributed systems than other known fairness notions because it provides an abstraction for stable property detection whereas the other fairness notions do not.>

In this paper, a new fairness notion is proposed for languages with multi-party interactions as the sole interprocess synchronization and communication primitive. The main advantage of this fairness notion is the elimination of starvation occurring solely due to race conditions (i.e., ordering of independent actions). Also, this is the first fairness notion for such languages which is fully-adequate with respect to the criteria presented in [AFK88]. The paper defines the notion, proves its properties, and presents examples of its usefulness.

Methods for synthesizing concurrent programs from Temporal Logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson & Clarke [EC82] and Manna & Wolper [MW84]. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. To synthesize a concurrent system consisting of K sequential processes, each having N states in its local transition diagram, requires construction of the global product-machine having at least NK global states in general. This exponential growth in K makes it infeasible to synthesize systems composed of more than 2 or 3 processes. In this paper, we show how to synthesize concurrent systems consisting of many (i.e., a finite but arbitrarily large number K of) similar sequential processes. Our approach avoids construction of the global product-machine for K processes; instead, it constructs a two process product-machine for a single pair of generic sequential processes. The method is uniform in K, providing a simple template that can be instantiated for each process to yield a solution for any fixed K. The method is also illustrated on synchronization problems from the literature.