Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

The inhibition spectrum and the achievement of causal consistency

Summary.  We consider the problem of distinguishing causally-consistent global states in asynchronous distributed systems. Such states are fundamental to asynchronous systems, because they correspond to possible simultaneous global states; their detection arises in a variety of distributed applications, including global checkpointing, deadlock detection, termination detection, and broadcasting. A consistent-cut protocol is a protocol which in every run will designate for each processor a state, in such a way that these states together form a consistent cut. We analyze the cost of achieving causal consistency in terms of the extent to which a consistent-cut protocol delays events of the underlying system. We refer to the delaying action of a protocol as inhibition. A protocol using local inhibition may cause the delay of some of a processor’s events until that processor has performed some number of local actions; a protocol using global inhibition may force the delay of some of a processor’s events until that processor has received some communication from other processors. Based on a variety of system and protocol characteristics, including the ability to locally or globally inhibit particular types of events, we give three impossibility results and examine some existing protocols. We are then able to present a thirty-six case summary of protocols and impossibility results for the determination of causally-consistent states as a function of those characteristics. In particular, we demonstrate that local inhibition is necessary and sufficient to solve this problem for general FIFO systems, while global send inhibition is necessary and sufficient for general non-FIFO systems. Received: January 1993 / Accepted: January 1996     

Exposure to deadlock for communicating processes is hard to detect

It is shown that the applicability of global state analysis as a tool for proving correctness of communication protocols is limited. Brand and Zafiropulo (1983) showed that reachability of global deadlock states for protocols with unbounded FIFO channels is undecidable. It is shown that the same is true for unbounded non-FIFO channels. For bounded FIFO channels the problem is shown to be PSPACE-hard.     

Arithmetic Meyer sets and finite automata

Non-standard number representation has proved to be useful in the speed-up of some algorithms, and in the modelization of solids called quasicrystals. Using tools from automata theory we study the set of β-integers, that is, the set of real numbers which have a zero fractional part when expanded in a real base β, for a given β > 1. In particular, when β is a Pisot number — like the golden mean —, the set is a Meyer set, which implies that there exists a finite set F (which depends only on β) such that . Such a finite set F, even of minimal size, is not uniquely determined.In this paper we give a method to construct the sets F and an algorithm, whose complexity is exponential in time and space, to minimize their size. We also give a finite transducer that performs the decomposition of the elements of as a sum belonging to .     

High-pain adaptive stabilization of multivariable linear systems — revisited

We consider the class of multi-input multi-output, finite dimensional, state space systems of the form , where the state dimension is unknown, the system is minumum phase, and it is known that det(CB) ≠ 0. For this class a universal adaptive high gain controller — not based on identification or estimation algorithms — is presented which ensures exponential decay of the motion of the closed-loop system. It is shown that the controller is robust with respect to certain nonlinear perturbations.     

Reverse reachability analysis: A new technique for deadlock detection on communicating finite state machines

The communicating finite state machines can exchange messages over bounded FIFO channels. In this paper, a new technique, called reverse reachability analysis, is proposed to detect deadlocks on the communication between the communicating finite state machines. The technique is based on finding reverse reachable paths starting from possible deadlock states. If a reverse reachable path can reach the initial global state, then deadlock occurs. Otherwise the communication is deadlock-free. The effectiveness of the technique has been verified by some real protocols such as a specification of X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.     

A note on the attractor-property of infinite-state Markov chains

In the past 5 years, a series of verification algorithms has been proposed for infinite Markov chains that have a finite attractor, i.e., a set that will be visited infinitely often almost surely starting from any state. In this paper, we establish a sufficient criterion for the existence of an attractor. We show that if the states of a Markov chain can be given levels (positive integers) such that the expected next level for states at some level n>0 is less than n−Δ for some positive Δ, then the states at level 0 constitute an attractor for the chain. As an application, we obtain a direct proof that some probabilistic channel systems combining message losses with duplication and insertion errors have a finite attractor.     

Common Knowledge and Update in Finite Environments

Logics of knowledge have been shown to provide a useful approach to the high level specification and analysis of distributed systems. It has been proposed that such systems can be developed using knowledge- based protocols, in which agents' actions have preconditions that test their state of knowledge. Both computer-assisted analysis of the knowledge properties of systems and automated compilation of knowledge-based protocols require the development of algorithms for the computation of states of knowledge. This paper studies one of the computational problems of interest, the model checking problem for knowledge formulae in the S5_nKripke structures generated by finite state environments in which states determine an observation for each agent. Agents are assumed to have perfect recall and may operate synchronously or asynchronously. It is shown that, in this setting, model checking of common knowledge formulae is intractable, but efficient incremental algorithms are developed for formulae containing only knowledge operators. Connections to knowledge updates and compilation of knowledge-based protocols are discussed.     

Verification of parametric concurrent systems with prioritised FIFO resource management

We consider the problem of parametric verification over a class of systems of processes competing for access to shared resources. We suppose the access to the resources to be controlled according to a FIFO-based policy with a possibility of distinguishing low-priority and high-priority resource requests. We propose a model of the concerned systems based on extended automata with queues. Over this model, we address verification of properties expressed in LTL∖X enriched with global process quantification and interpreted on finite as well as fair behaviours of the given systems. In addition, we examine parametric verification of process deadlockability too. By reducing the parametric verification problems to finite-state model checking, we establish several decidability results for different classes of the considered properties and systems (including the special case of systems with the pure FIFO resource management). Furthermore, we show that parametric verification against formulae with local process quantification is undecidable in the given context. This work was supported in part by the European Commission (FET project ADVANCE, contract No. IST-1999-29082), the French government by the project ACI Sécurité Informatique, the Czech Grant Agency (project 102/07/0322), the Czech-French Barrande project 2-06-27, and the Czech Ministry of Education within the project MSM 0021630528 “Security-Oriented Research in Information Technology”.     

Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

Verification of probabilistic systems with faulty communication

Many protocols are designed to operate correctly even in the case where the underlying communication medium is faulty. To capture the behavior of such protocols, Lossy Channel Systems (LCS’s) have been proposed. In an LCS the communication channels are modeled as unbounded FIFO buffers which are unreliable in the sense that they can nondeterministically lose messages. Recently, several attempts have been made to study Probabilistic Lossy Channel Systems (PLCS’s) in which the probability of losing messages is taken into account. In this article, we consider a variant of PLCS’s which is more realistic than those studied previously. More precisely, we assume that during each step in the execution of the system, each message may be lost with a certain predefined probability. We show that for such systems the following model-checking problem is decidable: to verify whether a linear-time property definable by a finite-state ω-automaton holds with probability one. We also consider other types of faulty behavior, such as corruption and duplication of messages, and insertion of new messages, and show that the decidability results extend to these models.     

On control of systems modelled as deterministic Rabin automata

Recent results on the control of infinite behaviour of finite automata are extended to allow Rabin acceptance conditions as modelling assumptions as well as specifications. The key result is a fixpoint characterization of the automaton'scontrollability subset—the set of states from which it can be controlled to the satisfaction of its associated specification. The fixpoint characterization allows for straightforward computation of the subset and for effective synthesis of controllers. the results have potential applications to supervisory control synthesis, the synthesis of reactive systems, and decision procedures for modal logics.     

Constraint-Based Verification of Parameterized Cache Coherence Protocols

We propose a new method for the parameterized verification of formal specifications of cache coherence protocols. The goal of parameterized verification is to establish system properties for an arbitrary number of caches. In order to achieve this purpose we define abstractions that allow us to reduce the original parameterized verification problem to a control state reachability problem for a system with integer data variables. Specifically, the methodology we propose consists of the following steps. We first define an abstraction in which we only keep track of the number of caches in a given state during the execution of a protocol. Then, we use linear arithmetic constraints to symbolically represent infinite sets of global states of the resulting abstract protocol. For reasons of efficiency, we relax the constraint operations by interpreting constraints over real numbers. Finally, we check parameterized safety properties of abstract protocols using symbolic backward reachability, a strategy that allows us to obtain sufficient conditions for termination for an interesting class of protocols. The latter problem can be solved by using the infinite-state model checker HyTech: Henzinger, Ho, and Wong-Toi, A model checker for hybrid systems, Proc. of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science, Springer, Haifa, Israel, 1997, Vol. 1254, pp. 460–463. HyTech handles linear arithmetic constraints using the polyhedra library of Halbwachs and Proy, Verification of real-time systems using linear relation analysis, Formal Methods in System Design, Vol. 11, No. 2, pp. 157–185, 1997. By using this methodology, we have automatically validated parameterized versions of widely implemented write-invalidate and write-update cache coherence protocols like Synapse, MESI, MOESI, Berkeley, Illinois, Firefly and Dragon (Handy, The Cache Memory Book, Academic Press, 1993). With this application, we have shown that symbolic model checking tools like HyTech, originally designed for the verification of hybrid systems, can be applied successfully to new classes of infinite-state systems of practical interest.     

Maximal versus strong solution to algebraic Riccati equations arising in infinite Markov jump linear systems

We deal with a perturbed algebraic Riccati equation in an infinite dimensional Banach space which appears, for instance, in the optimal control problem for infinite Markov jump linear systems (from now on iMJLS). Infinite or finite here has to do with the state space of the Markov chain being infinite countable or finite (see, e.g., [M.D. Fragoso, J. Baczynski, Optimal control for continuous time LQ—problems with infinite Markov jump parameters, SIAM J. Control Optim. 40(1) (2001) 270–297]). By using a certain concept of stochastic stability (a sort of L₂-stability), we have proved in [J. Baczynski, M.D. Fragoso, Maximal solution to algebraic Riccati equations linked to infinite Markov jump linear systems, Internal Report LNCC, no. 6, 2006] existence (and uniqueness) of maximal solution for this class of equations. As it is noticed in this paper, unlike the finite case (including the linear case), we cannot guarantee anymore that maximal solution is a strong solution in this setting. Via a discussion on the main mathematical hindrance behind this issue, we devise some mild conditions for this implication to hold. Specifically, our main result here is that, under stochastic stability, along with a condition related with convergence in the infinite dimensional scenario, and another one related to spectrum—weaker than spectral continuity—we ensure the maximal solution to be also a strong solution. These conditions hold trivially in the finite case, allowing us to recover the result of strong solution of [C.E. de Souza, M.D. Fragoso, On the existence of maximal solution for generalized algebraic Riccati equations arising in stochastic control, Systems Control Lett. 14 (1990) 233–239] set for MJLS. The issue of whether the convergence condition is restrictive or not is brought to light and, together with some counterexamples, unveil further differences between the finite and the infinite countable case.     

Local and global controllability for nonlinear systems

A technique to study local and global controllability properties for a wide class of nonlinear systems is presented. In addition to an extensive study of systems on ² we propose — as an application of our method — a new criterion for global controllability of systems with polynomial drift term, defined on ⁿ. In the case of linear systems, the criterion reduces to the classical Kalman condition.A study of local controllability at the equilibrium point of the drift term of systems defined on ² enables us not only to rederive a local controllability result derived by Hermes [4,5], but also to extend this result when no assumptions are made on the boundedness of the controls.     

Implementation of hierarchical F-channels for high-performance distributed computing

Summary High performance distributed computing systems require high performance communication systems.F-channels andHierarchical F-channels address this need by permitting a high level of concurrency like non-FIFO channels while retaining the simplicity of FIFO channels critical to the design and proof of many distributed algorithms. In this paper, we present counter-based implementations for F-channels and Hierarchical F-channels using message augmentation-appending control information to a message. These implementations guarantee that no messages are unnecessarily delayed at the receiving end. Keith Shafer received the B.A. degree in computer science and mathematics in 1986 from Mount Vernon Nazarene College, Mount Vernon, Ohio, USA, and the M.S. and Ph.D. degrees in computer science from The Ohio State University, Columbus, Ohio, USA, in 1988 and 1992, respectively. He is currently a Senior Research Scientist at OCLC Online Computer Library Center Inco, Dublin, OH, USA. His research interests include tools for comparing logical channels and methods for automatically constructing corpus grammars from tagged documents as an aid for database preparation and document conversion. Dr. Shafer is a member of the IEEE Computer Society. Mohan Ahuja received the M.A. degree in 1983 and the Ph.D. degree in 1985, both in computer science, from the University of Texas at Austin. He is currently with Department of Computer Science and Engineering, Univ. of California, San Diego. His recent research contributions include Global Flushing, message receipt in Receive-Phases, Incremental Publication of a Partial Order, Design of Highways (a high-performance distributed programming system) and — in collaboration with others — Passive-space and Time View, Performance evaluation of F-Channels, and Units of Computation in Fault-Tolerant Distributed Systems. His current research interests are in high-performance distributed communication and computing architectures, building high-performance systems, distributed operating systems, distributed algorithms, fault tolerance, and performance evaluation.Parts of this paper appeared in two conference papers, (1) Distributed Modeling and Implementation of High Performance Communication Architectures, in proceedings of the Thirteenth IEEE International Conference on Distributed Computing Systems, papes 56–65, 1993 and (2) Process-Channel_agem-Process model of asynchronous distributed communication, in proceedings of the Twelfth IEEE International Conference on Distributed Computing Systems, pages 4–11, 1992     

Assume,guarantee or repair: a regular framework for non regular properties

We present Assume-Guarantee-Repair (AGR)—a novel framework which verifies that a program satisfies a set of properties and also repairs the program in case the verification fails. We consider communicating programs—these are simple C-like programs, extended with synchronous actions over communication channels. Our method, which consists of a learning-based approach to assume–guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the required properties, or alters the system in a way that brings it closer to satisfying the properties. To handle infinite-state systems we build finite abstractions, for which we check the satisfaction of complex properties that contain first-order constraints, using both syntactic and semantic-aware methods. We implemented AGR and evaluated it on various communication protocols. Our experiments present compact proofs of correctness and quick repairs.