Abstract Alternating systems are models of computer programs whose behavior is governed by the actions of multiple agents with, potentially, different goals. Examples include control systems, resource schedulers, security protocols, auctions and election mechanisms. Proving properties about such systems has emerged as an important new area of study in formal verification, with the development of logical frameworks such as the alternating temporal logic ATL *. Techniques for model checking ATL * over finite-state systems have been well studied, but many important systems are infinite-state and thus their verification requires, either explicitly or implicitly, some form of deductive reasoning. This paper presents a theoretical framework for the analysis of alternating infinite-state systems. It describes models of computation, of various degrees of generality, and alternating-time logics such as ATL * and its variations. It then develops a proof system that allows to prove arbitrary ATL * properties over these infinite-state models. The proof system is shown to be complete relative to validities in the weakest possible assertion language. The paper then derives auxiliary proof rules and verification diagrams techniques and applies them to security protocols, deriving a new formal proof of fairness of a multi-party contract signing protocol where the model of the protocol and of the properties contains both game-theoretic and infinite-state (parameterized) aspects.

General solutions to deadlock avoidance in distributed systems are considered impractical due to the high communication overhead. In previous work we showed that practical solutions exist when all possible sequences of resource requests are known a priori in the form of call graphs; in this case protocols can be constructed that involve no communication. These run-time protocols make use of annotations of the call graph that are computed statically based on the structure of the call graph. If the annotations are acyclic, then deadlocks are unreachable. This paper focuses on the computation of these annotations. We first show that our algorithm for computing acyclic annotations is complete: every optimal annotation can be generated. We then show that, given a cyclic annotation and a fixed set of resources, checking whether deadlocks are reachable is NP-complete. Finally, we consider the problem of computing minimal annotations that satisfy given constraints on the number of available resources. We show that the problem is NP-complete in the general case, but that it can be solved in polynomial time if the only restrictions are that the number of certain resources is 1, that is, these resources are binary semaphores.

We present a deadlock avoidance algorithm for distributed systems that guarantees liveness. Deadlock avoidance in distributed systems is a hard problem and general solutions are considered impractical due to the high communication overhead. In previous work, however, we showed that practical solutions exist when all possible sequences of resource requests are known a priori in the form of call graphs; in this case protocols can be constructed that perform safe resource allocation based on local data only, that is, no communication between components is required. While avoiding deadlock, those protocols, however, did not avoid starvation: they guaranteed that some process could always make progress, but did not guarantee that every individual process would always eventually terminate. In this paper we present a resource allocation mechanism that avoids deadlock and guarantees absence of starvation, without undue loss of concurrency. The only assumption we make is that the local scheduler is fair. We prove the correctness of the algorithm and show how it can be implemented efficiently.

Distributed real-time and embedded (DRE) systems have stringent constraints on timeliness and other properties whose assurance is crucial to correct system behavior. Formal tools and techniques play a key role in verifying and validating system properties. However, many DRE systems are built using middleware frameworks that have grown increasingly complex to address the diverse requirements of a wide range of applications. How to apply formal tools and techniques effectively to these systems, given the range of middleware configuration options available, is therefore an important research problem.This paper makes three contributions to research on formal verification and validation of middleware-based DRE systems. First, it presents a reusable library of formal models we have developed to capture essential timing and concurrency semantics of foundational middleware building blocks provided by the ACE framework. Second, it describes domain-specific techniques to reduce the cost of checking those models while ensuring they remain valid with respect to the semantics of the middleware itself. Third, it presents a verification and validation case study involving a gateway service, using our models.

Thread allocation is an important problem in distributed real-time and embedded (DRE) systems. A thread allocation policy that is too liberal may cause deadlock, while a policy that is too conservative limits potential parallelism, thus wasting resources. However, achieving (globally) optimal thread utilization, while avoiding deadlock, has been proven impractical in distributed systems: it requires too much communication between components. In previous work we showed that efficient local thread allocation protocols are possible if the protocols are parameterized by global static data, in particular by an annotation of the global call graph of all tasks to be performed by the system. We proved that absence of cyclic dependencies in this annotation guarantees absence of deadlock. In this paper we present an algorithm to compute optimal annotations, that is annotations that maximize parallelism while satisfying the condition of acyclicity. Moreover, we show that the condition of acyclicity is in fact tight and exhibits a rather surprising anomaly: if a cyclic dependency is present in the annotation of the call graph and a certain minimum number of threads is provided, deadlock is reachable. Thus, in the presence of cyclic dependencies, increasing the number of threads may introduce the possibility of deadlock in an originally deadlock free system.

We present a specification language and algorithms for the online and offline monitoring of synchronous systems including circuits and embedded systems. Such monitoring is useful not only for testing, but also under actual deployment. The specification language is simple and expressive; it can describe both correctness/failure assertions along with interesting statistical measures that are useful for system profiling and coverage analysis. The algorithm for online monitoring of queries in this language follows a partial evaluation strategy: it incrementally constructs output streams from input streams, while maintaining a store of partially evaluated expressions for forward references. We identify a class of specifications, characterized syntactically, for which the algorithm's memory requirement is independent of the length of the input streams. Being able to bound memory requirements is especially important in online monitoring of large input streams. We extend the concepts used in the online algorithm to construct an efficient offline monitoring algorithm for large traces. We have implemented our algorithm and applied it to two industrial systems, the PCI bus protocol and a memory controller. The results demonstrate that our algorithms are practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.

We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over polynomial rings to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has been focussed on the construction of linear invariants for linear programs. Consequently, there has been little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.

Abstract. STeP, the Stanford Temporal Prover, supports the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [MBB99]. Automated model checking is combined with computer-aided deductive methods to allow for the verification of a broad class of systems, including parameterised ( N -component) circuit designs, parameterised ( N -process) programs, and programs with infinite data domains.