The recent extensive availability of "big data" platforms calls for a widespread adoption by the formal verification community. Cloud computing platforms represent a great opportunity to run massively parallel jobs, yet classical formal verification tools techniques must undergo a deep technological transformation in order to exploit the new available architectures. This has raised an increasing interest in deploying verification techniques on parallel distributed frameworks. In this paper we introduce a framework to ease the adoption of a distributed approach to verification of Computation Tree Logic (CTL) formulas on very large state spaces. The approach exploits integrates a recently developed, parametric state-space builder. The whole framework adopts M AP R EDUCE as core computational model, and can be tailored to different modelling formalisms. The outcomes of several tests performed on (Petri-nets based) benchmark specifications are presented, thus showing the convenience of the proposed approach.
The main idea of distributed algorithms for both LTL and CTL model checking is in fact similar: the state graph is partitioned among the network nodes, each network node owns a subset of the state space. The differences are in the way the state space is partitioned (through a ): this is a crucial issue. In order to increase performance of the parallel model checking, it is key to achieve a good load balancing among machines, meaning that each partition should contain nearly the same number of states. The performance of these algorithms depends also on the number of cross-border transitions of the partitioned state space ( transitions having the source state in a component and the target state in another component). This number should be as small as possible, since it has an effect on the number of messages sent over the network during the analysis @cite_24 . In the context of LTL model checking, probabilistic techniques to partition the state space have been used, for example, in @cite_29 @cite_19 , and a technique that exploits some structural properties derived from the verified formula has been proposed in @cite_5 .
@cite_24 @cite_19 @cite_29 @cite_5
2081955678 2488874620 1548575501 122407544
As model checking becomes increasingly used in industry, there is a big need for efficient new methods to deal with the large real-size designs. The author presents a novel method for improving the performance of model checking using parallelisation techniques. The model checking is performed on a distributed-memory environment consisting of a network of machines. The important two keys to focus on are the memory balance and communication reduction. A new algorithm for partitioning the large state space modelling industrial designs with hundreds of millions of states and transitions is proposed. The state space is supposed to be represented by a weighted Kripke structure (this is an extension of the Kripke structure where weights are associated with the states and with the transitions). This algorithm partitions the weighted Kripke structure by performing a combination of abstraction-partition-refinement on this structure. The CTL model checking algorithm is distributed on processes located on different network machines. Each one owns a partition and executes the algorithm on it. The algorithm for CTL model checking is designed to reduce the communication overhead between the processes. The experimental results on large real designs show that this method improves the quality of partitions, the communication overhead and then the overall performance of the model checking. We consider the following problem: given a linear system and a linear temporal logic (LTL) formula over a set of linear predicates in its state variables, find a feedback control law with polyhedral bounds and a set of initial states so that all trajectories of the closed loop system satisfy the formula. Our solution to this problem consists of three main steps. First, we partition the state space in accordance with the predicates in the formula, and construct a transition system over the partition quotient, which captures our capability of designing controllers. Second, using a procedure resembling model checking, we determine runs of the transition system satisfying the formula. Third, we generate the control strategy. Illustrative examples are included. Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics monadic second-order logic (MSO) and LTL as a natural logic for expressing the temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a buchi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature. In this paper, we propose a distributed algorithm for CTL model-checking and a counterexample search whenever the CTL formula is not satisfied. The distributed approach is used in order to cope with the state space explosion problem. A cluster of workstations performs collaborative verification over a partitioned state space. Thus, every process involved in the distributed verification performs the labelling procedure on its own partial state space, and uses the parse tree of the CTL formula to evaluate sub-formulas and delay the synchronisations so as to minimise idle time. A counterexample search consists in a distributed construction of the tree-like corresponding to the failure executions. Some experiments have been carried out to evaluate the efficiency of this approach. In this paper we discuss the problem of performing distributed CTL model checking by splitting the given state space into several "partial state spaces." The partial state space is modelled as a Kripke structure with border states. Each computer involved in the distributed computation owns a partial state space and performs a model-checking algorithm on this incomplete structure. To be able to proceed, the border states are augmented by assumptions about truth values of formulas and the computers exchange assumptions about relevant states to compute more precise information. This work puts forward a novel technique to generate finite abstractions of autonomous and nonautonomous Max-Plus-Linear (MPL) models, a class of discrete-event systems used to characterize the dynamics of the timing related to successive events that synchronize autonomously. Nonautonomous versions of MPL models embed within their dynamics nondeterminism, namely a signal choice that is usually regarded as an exogenous control or schedule. In this paper, abstractions of MPL models are characterized as finite-state Labeled Transition Systems (LTS). LTS are obtained first by partitioning the state space (and, for the nonautonomous model, by covering the input space) of the MPL model and by associating states of the LTS to the introduced partitions, then by defining relations among the states of the LTS based on dynamical transitions between the corresponding partitions of the MPL state space, and finally by labeling the LTS edges according to the one-step timing properties of the events of the original MPL model. In order to establish formal equivalences, the finite abstractions are proven to either simulate or to bisimulate the original MPL model. This approach enables the study of general properties of the original MPL model by verifying (via model checking) equivalent logical specifications over the finite LTS abstraction. The computational aspects related to the abstraction procedure are thoroughly discussed and its performance is tested on a numerical benchmark. Model checking became a standard method of analyzing complex systems in many application domains. No doubt, a number of applications is placing great demands on model checking tools. The process of analysis of complex and real-life systems often requires vast computation resources, memory in particular. This phenomenon, referred to as the state space explosion problem, has been tackled by many researchers during the past two decades. A plethora of more or less successful techniques to fight the problem have been introduced, including parallel and distributed-memory processing. DiVinE is a tool for LTL model checking and reach ability analysis of discrete distributed systems. The tool is able to efficiently exploit the aggregate computing power of multiple network-interconnected multi-cored workstations in order to deal with extremely large verification tasks. As such it allows to analyze systems whose size is far beyond the size of systems that can be handled with regular sequential tools. While the main focus of the tool is on high-performance explicit state model checking, an emphasis is also put on ease of deployment and usage. Additionally, the component architecture and publicly available source code of Divine allow for its usage as a platform for research on parallel and distributed-memory model checking techniques. The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems . Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp. We present a novel approach to proving the absence of timing channels. The idea is to partition the programâ s execution traces in such a way that each partition component is checked for timing attack resilience by a time complexity analysis and that per-component resilience implies the resilience of the whole program. We construct a partition by splitting the program traces at secret-independent branches. This ensures that any pair of traces with the same public input has a component containing both traces. Crucially, the per-component checks can be normal safety properties expressed in terms of a single execution. Our approach is thus in contrast to prior approaches, such as self-composition, that aim to reason about multiple (kâ � 2) executions at once. We formalize the above as an approach called quotient partitioning, generalized to any k-safety property, and prove it to be sound. A key feature of our approach is a demand-driven partitioning strategy that uses a regex-like notion called trails to identify sets of execution traces, particularly those influenced by tainted (or secret) data. We have applied our technique in a prototype implementation tool called Blazer, based on WALA, PPL, and the brics automaton library. We have proved timing-channel freedom of (or synthesized an attack specification for) 24 programs written in Java bytecode, including 6 classic examples from the literature and 6 examples extracted from the DARPA STAC challenge problems. Balanced graph partitioning is a well known NP-complete problem with a wide range of applications. These applications include many large-scale distributed problems including the optimal storage of large sets of graph-structured data over several hosts-a key problem in today's Cloud infrastructure. However, in very large-scale distributed scenarios, state-of-the-art algorithms are not directly applicable, because they typically involve frequent global operations over the entire graph. In this paper, we propose a fully distributed algorithm, called JA-BE-JA, that uses local search and simulated annealing techniques for graph partitioning. The algorithm is massively parallel: there is no central coordination, each node is processed independently, and only the direct neighbors of the node, and a small subset of random nodes in the graph need to be known locally. Strict synchronization is not required. These features allow JA-BE-JA to be easily adapted to any distributed graph-processing system from data centers to fully distributed networks. We perform a thorough experimental analysis, which shows that the minimal edge-cut value achieved by JA-BE-JA is comparable to state-of-the-art centralized algorithms such as METIS. In particular, on large social networks JA-BEJA outperforms METIS, which makes JA-BE-JA-a bottom-up, self-organizing algorithm-a highly competitive practical solution for graph partitioning. The graph-partitioning problem is to divide a graph into several pieces so that the number of vertices in each piece is the same within some defined tolerance and the number of cut edges is minimised. Important applications of the problem arise, for example, in parallel processing where data sets need to be distributed across the memory of a parallel machine. Very effective heuristic algorithms have been developed for this problem which run in real-time, but it is not known how good the partitions are since the problem is, in general, NP-complete. This paper reports an evolutionary search algorithm for finding benchmark partitions. A distinctive feature is the use of a multilevel heuristic algorithm to provide an effective crossover. The technique is tested on several example graphs and it is demonstrated that our method can achieve extremely high quality partitions significantly better than those found by the state-of-the-art graph-partitioning packages. We present Schism, a novel workload-aware approach for database partitioning and replication designed to improve scalability of shared-nothing distributed databases. Because distributed transactions are expensive in OLTP settings (a fact we demonstrate through a series of experiments), our partitioner attempts to minimize the number of distributed transactions, while producing balanced partitions. Schism consists of two phases: i) a workload-driven, graph-based replication partitioning phase and ii) an explanation and validation phase. The first phase creates a graph with a node per tuple (or group of tuples) and edges between nodes accessed by the same transaction, and then uses a graph partitioner to split the graph into k balanced partitions that minimize the number of cross-partition transactions. The second phase exploits machine learning techniques to find a predicate-based explanation of the partitioning strategy (i.e., a set of range predicates that represent the same replication partitioning scheme produced by the partitioner). The strengths of Schism are: i) independence from the schema layout, ii) effectiveness on n-to-n relations, typical in social network databases, iii) a unified and fine-grained approach to replication and partitioning. We implemented and tested a prototype of Schism on a wide spectrum of test cases, ranging from classical OLTP workloads (e.g., TPC-C and TPC-E), to more complex scenarios derived from social network websites (e.g., Epinions.com), whose schema contains multiple n-to-n relationships, which are known to be hard to partition. Schism consistently outperforms simple partitioning schemes, and in some cases proves superior to the best known manual partitioning, reducing the cost of distributed transactions up to 30 . Natural graphs, such as social networks, email graphs, or instant messaging patterns, have become pervasive through the internet. These graphs are massive, often containing hundreds of millions of nodes and billions of edges. While some theoretical models have been proposed to study such graphs, their analysis is still difficult due to the scale and nature of the data. We propose a framework for large-scale graph decomposition and inference. To resolve the scale, our framework is distributed so that the data are partitioned over a shared-nothing set of machines. We propose a novel factorization technique that relies on partitioning a graph so as to minimize the number of neighboring vertices rather than edges across partitions. Our decomposition is based on a streaming algorithm. It is network-aware as it adapts to the network topology of the underlying computational hardware. We use local copies of the variables and an efficient asynchronous communication protocol to synchronize the replicated values in order to perform most of the computation without having to incur the cost of network communication. On a graph of 200 million vertices and 10 billion edges, derived from an email communication network, our algorithm retains convergence properties while allowing for almost linear scalability in the number of computers. We use hybrid-systems techniques for the analysis of reachability properties of a class of piecewise-affine (PA) differential equations that are particularly suitable for the modeling of genetic regulatory networks. More specifically, we introduce a hyperrectangular partition of the state space that forms the basis for a discrete abstraction preserving the sign of the derivatives of the state variables. The resulting discrete transition system provides a qualitative description of the network dynamics that is well-adapted to available experimental data and that can be efficiently computed in a symbolic manner from inequality constraints on the parameters. We study the problem of model checking software product line (SPL) behaviours against temporal properties. This is more difficult than for single systems because an SPL with n features yields up to 2n individual systems to verify. As each individual verification suffers from state explosion, it is crucial to propose efficient formalisms and heuristics. We recently proposed featured transition systems (FTS), a compact representation for SPL behaviour, and defined algorithms for model checking FTS against linear temporal properties. Although they showed to outperform individual system verifications, they still face a state explosion problem as they enumerate and visit system states one by one. In this paper, we tackle this latter problem by using symbolic representations of the state space. This lead us to consider computation tree logic (CTL) which is supported by the industry-strength symbolic model checker NuSMV. We first lay the foundations for symbolic SPL model checking by defining a feature-oriented version of CTL and its dedicated algorithms. We then describe an implementation that adapts the NuSMV language and tool infrastructure. Finally, we propose theoretical and empirical evaluations of our results. The benchmarks show that for certain properties, our algorithm is over a hundred times faster than model checking each system with the standard algorithm. k−2 � 1 − xb−k � � dx� . Call this process a � -coalescent. Discrete measure-valued processes derived from the � -coalescent model a system of masses undergoing coalescent collisions. Kingman's coalescent, which has numerous applications in population genetics, is the δ0-coalescent for δ0 a unit mass at 0. The coalescent recently derived by Bolthausen and Sznit- man from Ruelle's probability cascades, in the context of the Sherrington- Kirkpatrick spin glass model in mathematical physics, is the U-coalescent for U uniform on � 0� 1� .F or� = U, and whenever an infinite number of masses are present, each collision in a � -coalescent involves an infinite number of masses almost surely, and the proportion of masses involved exists as a limit almost surely and is distributed proportionally to � . The two-parameter Poisson-Dirichlet family of random discrete distributions derived from a stable subordinator, and corresponding exchangeable ran- dom partitions ofgoverned by a generalization of the Ewens sampling formula, are applied to describe transition mechanisms for processes of coalescence and fragmentation, including the U-coalescent and its time reversal. 1. Introduction. Markovian coalescent models for the evolution of a sys- tem of masses by a random process of binary collisions were introduced by Marcus (29) and Lushnikov (28). See (3) for a recent survey of the scientific lit- erature of these models and their relation to Smoluchowski's mean-field theory of coagulation phenomena. Evans and Pitman (15) gave a general framework for the rigorous construction of partition-valued and discrete measure-valued coalescent Markov processes allowing infinitely many massses and treated the binary coalescent model where each pair of masses x and y is subject to a coa- lescent collision at rate κ� xyfor a suitable rate kernel κ. This paper studies a family of partition-valued Markov processes, with state space the compact set of all partitions of � �= � 1� 2 ���� � , such that the restriction of the partition to each finite subset ofis a Markov chain with transition rates of a simple form determined by the moments of a finite measureon the unit interval. The case � = δ 0 , a unit mass at 0, is Kingman's coalescent in which every Billion-node graphs pose significant challenges at all levels from storage infrastructures to programming models. It is critical to develop a general purpose platform for graph processing. A distributed memory system is considered a feasible platform supporting online query processing as well as offline graph analytics. In this paper, we study the problem of partitioning a billion-node graph on such a platform, an important consideration because it has direct impact on load balancing and communication overhead. It is challenging not just because the graph is large, but because we can no longer assume that the data can be organized in arbitrary ways to maximize the performance of the partitioning algorithm. Instead, the algorithm must adopt the same data and programming model adopted by the system and other applications. In this paper, we propose a multi-level label propagation (MLP) method for graph partitioning. Experimental results show that our solution can partition billion-node graphs within several hours on a distributed memory system consisting of merely several machines, and the quality of the partitions produced by our approach is comparable to state-of-the-art approaches applied on toy-size graphs. Graph partitioning requires the division of a graph's vertex set into k equally sized subsets s.t. some objective function is optimized. High-quality partitions are important for many applications, whose objective functions are often NP-hard to optimize. Most state-of-the-art graph partitioning libraries use a variant of the Kernighan-Lin (KL) heuristic within a multilevel framework. While these libraries are very fast, their solutions do not always meet all user requirements. Moreover, due to its sequential nature, KL is not easy to parallelize. Its use as a load balancer in parallel numerical applications therefore requires complicated adaptations. That is why we developed previously an inherently parallel algorithm, called Bubble-FOS C [H. Meyerhenke, B. Monien, S. Schamberger, Accelerating shape optimizing load balancing for parallel FEM simulations by algebraic multigrid, in: Proceedings of the 20th IEEE International Parallel and Distributed Processing Symposium, IPDPS'06, IEEE Computer Society, 2006, p. 57 (CD)], which optimizes partition shapes by a diffusive mechanism. However, it is too slow for practical use, despite its high solution quality. In this paper, besides proving that Bubble-FOS C converges towards a local optimum of a potential function, we develop a much faster method for the improvement of partitionings. This faster method called TruncCons is based on a different diffusive process, which is restricted to local areas of the graph and also contains a high degree of parallelism. By coupling TruncCons with Bubble-FOS C in a multilevel framework based on two different hierarchy construction methods, we obtain our new graph partitioning heuristic DibaP. Compared to Bubble-FOS C, DibaP shows a considerable acceleration, while retaining the positive properties of the slower algorithm. Experiments with popular benchmark graphs show that DibaP computes consistently better results than the state-of-the-art libraries METIS and JOSTLE. Moreover, with our new algorithm, we have improved the best known edge-cut values for a significant number of partitionings of six widely used benchmark graphs. In this paper we propose a distributed algorithm for model-checking LTL formulas that works on a network of workstations and effectively uses the decomposition of the formula automaton to strongly connected components to achieve more efficient distribution of the verification problem. In particular, we explore the possibility of performing a distributed nested depth-first search algorithm. The NP-hard graph partitioning problem is an important subtask in load balancing and many other applications. It requires the division of a graph's vertex set into P equally sized subsets such that some objective function is optimized. State-of-the-art libraries addressing this problem show several deficiencies: they are hard to parallelize, focus on small edge-cuts instead of few boundary vertices, and often produce disconnected partitions. This work introduces our novel graph partitioning and repartitioning heuristic Bubble-FOS C. In contrast to other libraries, Bubble-FOS C does not try to minimize the edge-cut explicitly, but focuses instead implicitly on good partition shapes. The shapes are optimized by diffusion processes that are embedded into an iterative framework. This approach incorporates a high degree of parallelism. Besides describing the evolution process that led to the new diffusion scheme FOS C used by Bubble-FOS C, we reveal some of FOS C's properties and propose a number of enhancements for a fast and reliable implementation. Our experiments, in which we compare sequential and parallel Bubble-FOS C implementations to the state-of-the-art libraries Metis and Jostle, reveal that our new heuristic is slower, but generates high-quality solutions that are often superior.