We introduce a variant of a formalism appearing in recent work geared towards modelling systems in which a distinguished entity (leader) orchestrates the operation of an arbitrary number of identical entities (followe...
详细信息
We introduce a variant of a formalism appearing in recent work geared towards modelling systems in which a distinguished entity (leader) orchestrates the operation of an arbitrary number of identical entities (followers). Our variant is better suited for the verification of system properties involving complex arithmetic conditions. Whereas the original formalism is translated into a tractable fragment of first-order temporal logic, aiming to utilize automated (first-order temporal logic) theorem provers for verification, our variant is translated into linear integer arithmetic, aiming to utilize satisfiability modulo theories (SMT) solvers for verification. In particular, for any given system specified in our formalism, we prove, for any natural number n, the existence of a linear integer arithmetic formula whose models are in one-to-one correspondence with certain counting abstractions (profiles) of executions of the system for n time steps. Thus, one is able to verify, for any natural number n, that all executions for n time steps of any such system have a given property by establishing that said formula logically entails the property. To highlight the practical utility of our approach, we specify and verify three consensus protocols, actively used in distributed database systems and low-power wireless networks.
We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to...
详细信息
ISBN:
(纸本)9783031826993;9783031827006
We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to decide a wide range of verification problems, including control-state reachability, coverability, and target, in a fixed finite abstraction of the infinite state-space, called a 01-counter system. We show that several systems from the parameterized verification literature fall into this class, including reconfigurable broadcast networks (or systems with lossy broadcast), disjunctive systems, synchronizations and systems with a fixed number of shared finite-domain variables. Our framework provides a simple and unified explanation for the properties of these systems, which have so far been investigated separately. Additionally, it extends and improves on a range of the existing results, and gives rise to other systems with similar properties.
The parameterized verification problem seeks to verify all members of some collection of systems. We consider the parameterized verification problem applied to systems that are composed of an arbitrary number of compo...
详细信息
The parameterized verification problem seeks to verify all members of some collection of systems. We consider the parameterized verification problem applied to systems that are composed of an arbitrary number of component processes, together with some fixed processes. The components are taken from one or more families, each family representing one role in the system;all components within a family are symmetric to one another. Processes communicate via synchronous message passing. In particular, each component process has an identity, which may be included in messages, and passed to third parties. We extend Abdulla et al.'s technique of view abstraction, together with techniques based on symmetry reduction, to this setting. We give an algorithm and implementation that allows such systems to be verified for an arbitrary number of components: we do this for both safety and deadlock-freedom properties. We apply the techniques to a number of examples. We can model both active components, such as threads, and passive components, such as nodes in a linked list: thus our approach allows the verification of unbounded concurrent datatypes operated on by an unbounded number of threads. We show how to combine view abstraction with additional techniques in order to deal with other potentially infinite aspects of the analysis: for example, we deal with potentially infinite specifications, such as a datatype being a queue;and we deal with unbounded types of data stored in a datatype.
parameterized verification is a challenging problem that is known to be undecidable in the general case. CMP is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 200...
详细信息
parameterized verification is a challenging problem that is known to be undecidable in the general case. CMP is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the CMP method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of CMP in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in CMP, as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of CMP to the FLASH cache coherence protocol.
We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety ve...
详细信息
ISBN:
(纸本)9781450392624
We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety verification problem undecidable. In the light of this result, we consider parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs combined with a fixed number of distinguished threads that are unrestricted. Our first contribution is an effective and simplified RA semantics for such systems. We leverage the simplified semantics to show that safety verification becomes PSPACE in the parameterized case, an optimistic result for algorithmic verification. Our proof uses an encoding to Datalog which, in addition to the complexity upper bound, suggests a verification algorithm based on Horn clause solvers. We also provide a matching lower bound showing that safety verification is PSPACE-hard.
We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers...
详细信息
We introduce a framework for the verification of protocols involving a distinguished machine (referred to as a leader) orchestrating the operation of an arbitrary number of identical machines (referred to as followers) in a network. At the core of our framework is a high-level formalism capturing the operation of these types of machines together with their network interactions. We show that this formalism automatically translates to a tractable form of first-order temporal logic. Checking whether a protocol specified in our formalism satisfies a desired property (expressible in temporal logic) then amounts to checking whether the protocol's translation in first-order temporal logic entails that property. Many different types of protocols used in practice, such as cache coherence, atomic commitment, consensus, and synchronization protocols, fit within our framework. First-order temporal logic also facilitates parameterized verification by enabling us to model such protocols abstractly without referring to individual machines.
We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and writ...
详细信息
We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go bey...
详细信息
The last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially permit modular, scalable verification approaches that mimic their modular design. We address this need for verification of distributed agreement-based systems through our novel modeling and verification framework, QUICKSILVER, that is not only modular, but also fully automated. The key enabling feature of QUICKSILVER is our encoding of abstractions of verified agreement protocols that facilitates modular, decidable, and scalable automated verification. We demonstrate the potential of QUICKSILVER by modeling and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more.
In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic Stat...
详细信息
In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.
parameterized verification is shown to be a complicated and undecidable problem. The challenge of parameterized verification lies in how to construct appropriate invariants. Designing algorithms to find such invariant...
详细信息
ISBN:
(纸本)9781538666487
parameterized verification is shown to be a complicated and undecidable problem. The challenge of parameterized verification lies in how to construct appropriate invariants. Designing algorithms to find such invariants automatically has become an active research area since the last decade. With the advent of some recent works, automatically finding invariants has become possible, but most of these invariants are unreadable, making them difficult to be understood by protocol designers and researchers. Therefore, we propose an automatic framework that learns a set of readable and simple invariants to support in protocol design. It takes advantage of association rule learning, and combines the learning algorithm with parameterized verification. It is noteworthy that the gap between machine learning algorithms and parameterized verification seems to be huge, as they rely on statistical learning and symbolic reasoning, respectively. Our framework, however, builds a bridge through association rules and invariants, making their combination possible. Besides, we also propose an invariant-guided strengthening paradigm, providing an innovative perspective to existing abstraction-strengthening methods. Our framework has been successfully applied to several benchmarks, including an industrial-scale protocol FLASH.
暂无评论