Distributed Verification on the Fly of Large State Spaces

Distributed Verification on the flyof Large State

Spaces

A Preprint

Mike Nkongolo

Faculty of Science

School of Computer Science and Applied Mathematics (Wits University, Johannesburg)

Laby Ilumbe

Department of Transport

and Supply Chain Management (University of Johannesburg)

Patrick Twite IlungaShenyang Aerospace university China

April 29, 2019

Abstract

This research is attempting to design and implement a generic infrastructure for distributed on− the− flyverification based on models allowing functional verification of competing complex systems. This work is part of the context Construction and Analysis of Distributed Processes for the design

of communication protocols and distributed systems. Whenever possible, we try to validate our proposals by developing tools, using the generic Open environment for exploration, in order to combine them with other existing tools and to allow direct interfacing with various specifications languages-these languages describe the source program to be evaluated. Applying these tools to complex, often industrial, case studies is an integral part of the process of validating the proposed methods. This systematic confrontation with implementation and experimentation problems is an essential aspect of our journey. The approach we have adopted is to address the traditional technical limitations of verifying the scaling up of programs to be audited. More precisely, we have pursued a twofold objective: i) by designing distributed algorithms containing one or more blocks of Boolean equations (with no mutually recursive inter-block dependencies), in order to increase the capacity of the resolution (currently limited there are about 108 variables on equals machines) using the computing and memory resources of a set of machines interconnected by a network. The implementation of these algorithms must have general programming interfaces that can be used by standard verification techniques and by all tools that have a connection to the Open / Caesar environment. ii) by designing and developing model-based translatable verification applications which directly benefit from the distributed resolution mechanisms proposed in the first objective. These audit tools should, as much as possible, be independent of the program description language to be verified, while having comparable performance to the best existing tools. The verification of finished state systems, whether distributed or competitive, is in practice confronted with the problem of state explosion (prohibitive size of space Vs Underlying states) that occur for realistic-sized systems that contain many parallel processes and complex data structures. Various techniques have been proposed to combat the explosion of states, such as on the fly verification and partial order reduction. However, practical experience has shown that none of these techniques, alone, is always sufficient to master large-scale systems. This paper proposes a combination of these approaches in order to scale up their auditing capabilities. Our approach is based on Boolean Equation Systems (BES) or B, which provide an elegant intermediate representation of verification problems defined on systems of Transitions Labeled, such as comparison by equivalence, evaluation of non-alternating modal µ-calculus formulas, or the generation of conformance test cases. We propose 1 algorithm

for BES such as distributed− flightresolution (containing one or more blocks of equations), and we use them as calculation engines for four on− the− flyverification tools developed within the CADPtoolbox using the Open / Caesar environment. Experimental measurements on clusters

of machines show near-linear acceleration and good scaling of distributed versions of these tools compared to their equivalents is sequential.

KeywordsSystem of Boolean equations, distributed memory algorithm, on-the-fly verification, equivalence comparison, partial order reduction, evaluation of temporal logic formulas, generation of conformity test cases

1. Introduction

Designing very wide computer systems (software or hardware architectures) which guaranteed to work properly, is still an unresolved goal despite decades of research in this direction [SVA, CJGK⁺18, SBF98]. Due to the omnipresence of computer systems in our society, the costs generated by faulty systems become alarming. In this paper, our goal is the detection of conceptual errors (or errors) in the realization of systems. Such mistakes often occur under unforeseeable circumstances, or too complicated to be discovered and understood by human beings. They occur, for example, when a program is run in a distributed environment. Exhaustively testing such programs is virtually impossible. The design of these systems requires methods and tools of verification, of which a widely recognized category is formal verification(see for instance [BT18]). Two major approaches exist in the field of formal auditing: the evidence − basedapproach and the model− basedapproach. The first one allows to deal with systems with an infinite number of states, but can not be completely automated. On the other hand, the model− basedmethod , although restricted to systems with a finite number of states, allows for a simpler and faster verification process, which does not require a high level of expertise on the part of the user. The approach we adopt is the model− orientedone, widely known in most engineering disciplines [BT18, Eas18]. Instead of directly constructing an object, we first conceive a model, which is analyzed and verified entirely. Once the model obtained and tested is satisfactory, the object can really be built and implemented. For very large computer systems, the model is an abstraction (or simplification) of the behavior of critical parts of the system, and the verification is to prove that the model satisfies all relevant properties. Formal method research has defined a complete set of notations to approximately describe all models we can design including all the interesting properties, behavioral and temporal properties. The essential quest that we must now fulfill is to prove that the system satisfies the required properties.

2. Verification of distributed programs

Verification Mechanism: verification is a process used to demonstrate the functional correction of a software design, usually described by means of a programming language or better, a high-level language ( or formal) having a well defined operating algorithm [RU19]. In the model-based approach, widely used because characterized by a good cost-performance trade-off, this description is then translated automatically to an underlying model, which is often a system of transitions labeled (STL), that is to say a graph (or automaton) containing, possibly with certain abstractions, all possible behaviors of the software system [RU19]. Verification then consists of comparing the model of the system with its specification or properties that describe the expected functioning of the system (or the services that it must provide), for example, the absence of blockage, mutual exclusion, equity, etc.

Verified properties: Depending on the nature of specification or formalism used to express properties, we can distinguish two types of approaches for verifying [Lam16]:

• Behavioral properties : they describe the functioning of the system in the form of automata(or using higher level descriptions that are then translated into automata). Since the system to be tested and its behavioral properties can both be represented by automata, the verification consists in comparing them by means of relations of equivalence,

• Logical properties: they characterize functional properties of the system, such as the absence of blocking, mutual exclusion, the correct transmission of the messages or the equitable access to resources. Among formalisms used, temporal logics, in particular the modal µ -calculus, are well adapted to describe the evolution

of the system over time. In this case, the check consists in ensuring that the automaton modeling the system satisfies a set of logical properties using tools called evaluators [BCM18].

States Explosions: although model-based verification techniques are efficient and fully automatable, their main limitation lies in the problem of state explosion, which occurs when the number of the state of the system exceeds capacity in the memory of the machine [SVA, CJGK⁺18, Eas18, BCM18]. State explosion is a combinatorial growth of the state space of a software system when it is composed of several asynchronous parallel components (interlacing

Illustrations are not included in the reading sample.

Figure 1: Distributed architecture composed of homogeneous machines interconnected by a network standard [JM06]

of actions during execution) and when manipulating complex data (a state being associated with each combination of possible values of these data). The explosion of the state space is the reason why the size of the systems that the verification tools can currently control is usually small, and for which many interesting applications still out of reach. Several partial solutions to this problem exist, such as the combination of verification techniques with graph manipulation techniques [CJGK⁺18].

Distributed Verification: the last few years have been rich in results of high-performance of scientific computation, which has continued to increase its importance in supporting Multi-disciplinary engineering explorations [KYF⁺12]. Since the scientific computation communities and formal methods have not traditionally worked together, there is very little work to describe possible interactions between different outcomes (theoretical and practical). An example of such interaction is the use of formal methods to verify software and hardware systems for high performance computing [RU19, Lam16, KYF⁺12]. Our study addresses the inverse problem, namely, the exploitation of potential computational power and parallelism of a Pcstack for the execution of application verification.

3. Distributed Architecture Model (DAM)

Our Distributed Machine Model is composed of Pdistributed computers loosely coupled, also called nodes. Each node, numbered from 1 to P, has its own processor (CPU) and its own memory. The interconnection between several nodesis realized by a high-speed network standard (see for instance [GMJD12]). We focus on such distributed memory architectures, such as clusters of cluster and workstation networks because they are accessible in local networks (Lans) of most research laboratories and companies. Another argument is that they are also very cheap, that they can evolve in computing power and in memory space easily, unlike multiprocessor, supercomputers are very powerful but very expensive and not very evolving. Figure 1 illustrates an example of the distributed architecture utilized.

The hypothesis we make on the network is that all machines can communicate two by two by exchanging messages with the Tcp / Ip protocol via sockets. About nodes, we assume that they are homogeneous in CPU, memory and operating system. This feature facilitates both the design of distributed algorithms, such as level of data distribution and task scheduling in heterogeneous architectures.

3.1 Performance measures

In many cases, the theoretical complexity in the worst case of a distributed algorithm is not a good indicator of its utility in practice. To show qualities of a distributed tool, performance measures are also performed, usually on the types of data for which the tool is designed (in our case, it is the state space corresponding to the system to be verified) [CJGK⁺18]. Two important measures for the practical performance of an algorithm (parallel or distributed) are used.

Illustrations are not included in the reading sample.

Figure 2: Syntax and semantics of the modal µ-calculus

Given a problem of verification, if T _tis the time taken by the best equation algorithm to solve the problem, and T _p the time taken by the distributed algorithm to solve the same problem on a machine distributed with Pnodes, acceleration SPand efficiency EPare defined as follows:

SP= Tt

T_p

(1)

4. µ-calculus

SP

EP=

P

(2)

The modal µ-calculus is an expressive logic, which can replace most temporal logic data in the literature. In its original version, the µ-calculus is interpreted on Kripkestructures K= (S; P; L; T). Modal formulas are defined on vocabularies, each action induces a binary relationship on Sthat connects the early states of the execution. Nevertheless, in a similar way to other temporal logics, it is possible to define semantics of formulas of modal µ-calculation on M= (Q; A; T; q₀). The syntax and semantics of the modal µ-calculus is defined in Figure 2.

4.1. Development of EVALUATOR 3.5-Connection

The Evaluator Tool has been developed within CADPusing the generic Open / Caesar environment for exploration. Evaluator (version 3: 5) consists of two parts: a front− part, responsible for the translation of modal µ-calculation formula 1 into a multiblock and the interpretation of counterexamples provided a resolution entry; and a rear− part, which carries the resolution and serves as a verifying engine. Successors of a Boolean variable Xqdenoting

satisfiabilityof modal µ-calculation formula on the state of the art is calculated by the front part of Evaluator which is termed equitably and independently on each worker node. In order to compare distributed versions (based on depth first traversal) of Evaluator, we have done a whole extensive experiments on different cases obtained from CADPcase studies. It should be noted that to obtain a precise image of performances, we exclude the costs (xes) system-dependent activities (code loading on remote nodes, initialization of connections), and we keep only the costs (variables) of the distributed resolution and terminating detection. We have done each experiment ten times. Each point of each curve corresponds to the average of the eight values corresponding to the measurements obtained, excluding the maximum values and minimal (see Figure 3).

Illustrations are not included in the reading sample.

Figure 3: Evaluator tool Architecture [JM06]

5. Distributed Programming Model

A clear distinction should be made at this level between parallelism − on− sharedmemory machines and parallelism− on− distributedmemory machines. The algorithms in the first category usually assume the presence of a single memory and several processors [NKVL19, RU19]. The number of processors available is about the size of the problem, whereas for distributed memory machines, the number of processors is much smaller and insignificant in relation to the size of the problem. Also, for the shared memory, the communication between processors is not a problem, whereas for the distributed memory, the latencyof communication plays an important role. Also, programs designed for shared memory can not easily be run on a shared memory machines, because, most of the time, the latencyis too high for a computer system which shared Virtual Memory (VM). By choosing a distributed memory architecture, we have naturally opted for specific models of programming and distributed algorithms based on the paradigm of transmission of messages. The resulting programs usually consist of a set of identical tasks on each of the nodes, and a set of data, disjoint two− to− twoon each of the nodes. This type of distributed programming is part of multiple instruction, and in this case, more specifically from the shared memory machines class, because one and the same program is executed on each of the nodes. However, this same program discerns asymmetric behavior for one of the processes performed. In fact, the first instance (also called supervisor) of our distributed program, has a totally orthogonal role compared to distributed computation [NKVL19, BCM18]. Its role is to initiate each instance of the program on the remote nodes, to set up the interconnections between nodes, to eventually collect statistics on the progress of the overall execution of the distributed program, and finally to allow interaction with the end user of the program, by means of an interface, for example by accessing queries for interrupting the calculation. Generally, such a process (also called Master) is executed on the user’s machine which does not need to be part of the set of homogeneous machines participating in the distributed calculation [Eas18, NKVL19]. An abstract representation of this network topology and the Pdistributed processes can be described by the left− handpart of Figure 3 and an example of a corresponding real-life practice by the right− handpart of the same figure.

Illustrations are not included in the reading sample.

Figure 4: Supervisor-worker abstract (a) and concrete (b) programming model [JM06]

5.1. Modeling Distributed Systems

In order to validate our distributed algorithms in the context of applications verification, it is necessary to introduce some additional notions about the systems that we want to verify as well as their formal representation in terms of models. Distributed applications (such as communication protocols and distributed systems) can be represented as asynchronous systems composed of several entities ("black boxes") which evolve competitively and communicate by exchanging messages. The behavior of such a system is described by the actions (or "events") that it performs during its execution. A peculiarity of such a formalism resides in the intertwining scheme, where several different actions can not be performed simultaneously. There are other semantics of parallelism, especially those used in synchronous languages, where several actions can occur at the same time. In this study, we will consider only descriptive− languageswith intertwined patterns, as they are more adapted to the model.

5.2. System of Transitions Labeled

In accordance with the interlacing scheme, the behavior of a parallel program can be naturally modeled by a graph(or automaton ) whose vertices represent the state of the program and arcs (or transitions) deny changes in the state of the program as a result of actions it performs during its execution. There are usually two classes of parallel program models, used depending on whether the relevant information is attached to program states or transitions: Kripke structures and systems. The formal definitions of these models are given below. We consider a set Qwhose elements are called states, a set Awhose elements are called actions, and a particular action, β, called invisible action or internal, and not included in A.

5.3. Definition-Kripkes structure

A Kripke Kstructure is a quadruplet (Q, P, L, T), where :

5.3.1. Qis a set of states, q1, q2, ...;

5.3.2. Pis a set of atomic propositions, noted p1, p2, ...;

5.3.3.L: Q→ 2^Pis associated with each state qand all atomic propositions satisfied by q

5.3.4. T⊆ Q∗ Qis the transition relationship

5.3.5. (q₁, q₂) ∈ βare called transitions

Illustrations are not included in the reading sample.

Figure 5: Transitions system representing the Bit Alternate protocol with two messages

A path φis a sequence (finite or infinite) q ₀ →q ₁ → ...of states. The sixth state of φis denoted by φ(k) and the highest sufficient (q _k → q_k+ → ...) of φ is denoted by φk. A path φis said to be maximal if it is infinite or terminated and its last state has no successor (that is, there is no state q∈ Qsuch that q _n → q).

5.4. Explicit and Implicit Representation

Explicit and implicit representation is an independent model of the source language describing the system to be verified. It is also independent of the tools of verification. An example of this is shown in Figure 5. It contains 12 states and 20 transitions, 4 action labels named PUT! 0, PUT! 1, GET! 0, GET! 1and finally an invisible action β(indicated by iin the figure). This example illustrates in an explicit way the state of a communication protocol with two different messages specified in a formal language. The size of the graph depends on the possible number of different messages exchanged.

Explicit representation: it consists of memorizing all states, actions and transition relationships of the system, as well as various other information from the source program from which it was generated (types and functions). The tools that exploit it can thus provide the user with accurate diagnostics in terms of the source program. This representation gives access to the values contained in the transitions states and labels, as well as to exploring the transition relation of the System (to the initial state, to the successors and predecessors of states and transitions).

Implicit representation: it consists in providing only the successor function of system. Such a successor function can be formally described in the following manner.

Q→ 2^A∗q(3)

(A, S^∗)|S→^aS ^∗ ∈ β(4)

The implicit representation access the initial state and the successor transitions of a given state for an efficient exploration which do not need to be implemented. Since we are looking to develop distributed algorithms to perform the on− the− flyverification of parallel programs, we will use the implicit representation of the system (and consequently of the system of Boolean equations), to carry out our verification, called in this case energeticverification, because we choose to explicitly generate states and transitions ( and not to group or merge them as in the symbolic methods). We are seeking to develop the most widely available on− the− fly verification tools available. One way to achieve this goal

is to use the Open / Caesar environment in the CADPtoolbox, which not only allows for on− the− flyexploration

(for simulation, verification or test generation tools) of programs from parallel programs, but also the independence of

the description language of these programs.

6. Literature Review

To address the limitation size of finite− statemodels that can be verified or processed by current techniques, we propose the distribution of the model and its treatment on a set of interconnected machines, in order to take advantage of computing power and memory globally augmented. This complementary solution to the techniques of minimization, of compositionalconstruction of the model or even of abstraction of the problem to be treated, allows an immediate gain in time and memory used by the machine, as well as the ability to deal with size− ableproblems. This technique is therefore very promising, processors are constantly improving and gaining efficiency. This section is dedicated to the literature with regards to the description of our algorithm for distributed resolution on the fly.

6.1. System of Boolean Equations

The first algorithms with a polynomial complexity to solve distributed resolution on the fly, were proposed by [Fer96], and [Lar92]. These algorithms were global, that is, they only required the system to be completely constructed before starting the resolution, and they calculated the solution for all variables of this System; the algorithms given in [Fer96, Lar92] have a linear complexity in the size (number of variables and operators). It happens very often that we are interested only in the resolution of a single variable, called the main variable or variable of interest, for example, when translating the problem of comparison in temporal logic. Research has been undertaken to design flight algorithms (local), which are able to calculate the value of a single variable by examining only the portions influencing this variable. The first algorithms on the flyto solve this problem have been proposed in [Ace94, AV95], and [Kei13]; the algorithms given in [LS98] have a linear complexity in the size. Another local algorithm in linear time, called Lmc, was proposed by [CDS00]: the algorithm accelerates the resolution by detecting components which are strongly related to the graph and variables and has been used successfully for the analysis of communication protocols of industrial size. The theory underlying distributed verification and their relation to modal logics and µ-calculus have been studied by [CDS00], who also proposed several efficient local and global algorithms based on methods of Gauss elimination. However, algorithms resolution and resources of computers currently available do not allow a scaling up of the resolution for large Systems (for example, containing more than 108 variables); as a result, distributed solutions is required. An alternative formulation of equivalence comparison and time logic verification in terms of game graphs has also been proposed by [YP19]. Recently, [VSA19, YP19, JKP19, BL19], have made use of game graphs as an intermediary representation of the problem of distributed (global and local) verification of temporal logic expressed in modal µ-calculus of alternation 1.

6.2. System of Boolean Equations

Let Xbe a set of Boolean variables. A system of Boolean Equations on Xis a tuple B= (X, M1, ..., Mn), where:

6.2.1. x∈ Xis a Boolean variable and

6.2.2. M _i= [x _j =^σiop_jX _j ∈ [1, m_i](i∈ [1, n])] are smaller equation blocks (or more big) sign fixed point

Figure 6 shows a system composed of three blocks of different polarities, two (M1 and M2) are defined by a smaller fixed point, and the third (M3) by a larger fixed point. This example shows a possible textual representation of a system for each Boolean variable used in the right part of a Boolean equation, the existence of a definition of this variable is in the left part. We created each external variables with regards to the current block, such as X4 and X7 in block M1. This class of the system, is convenient for designing algorithms for efficient resolution, while remaining general: any system containing combinations of dis-junctions and conjunctions in the right part of the equations can be made simple (at the cost of a linear increase in size) by factoring the sub formulas purely disjunctive or conjunctive.

6.3. Semantic of Boolean Equations

We call context σ, a partial function σ: x→ Bool , with Bool= [0,1] which associates a Boolean value to some elements of x. The semantic of a Boolean formula op_i [X ₁ →→→ X_k] in a context σ , giving a Boolean value to X ₁ →→→ ^→→→ X _kis the Boolean value defined as follows:

0p_i[x₁,→→→, x_k]σ= σ(x₁)op _i →→→ op_iσ(x_k) (5)

6.4. Local Resolution

Let the system of Boolean equations be B= [X, M ₁ →→→ M_n] alternate 1. The computation of a variable of a block is done usually according to the following algorithm:

6.4.1. A R _iroutine is associated with M_i,

Illustrations are not included in the reading sample.

Figure 6: An example of a multiblock system represented in textual form

Illustrations are not included in the reading sample.

Figure 7: A System of Boolean Equations, its Boolean graph, and the result of a local resolution for x ₁

6.4.2. R_i(X_j) calculates the value of X _jin M_i, by evaluating the straight parts of equations and substituting the calculated values,

6.4.3. The call stack R₁(X) →→→ R_n(X_n) is bounded by the depth of the graph of dependencies between blocks,

6.4.4. Each R _iretains its context, as in the case of co-routine.

This approach allows the system of Boolean equations Bto be built on the fly, and calculates only useful information for the final value of the variable of interest. Various strategies (for example, depth first [Str04]) can be used, giving algorithms of resolution with linear complexities in time and space. Figure 7 shows a System of Boolean Equations B with a semantic of larger fixed point, the corresponding Boolean graph, and a sub graph (included in the light gray surface) computed by an algorithm of local resolution (based on a Depth-First Search (DfS)) from the vertex x ₁ (the

white and black vertices denote the variables Tand F, respectively).

Another characteristic of local resolution methods is the generation of diagnostics (portions of Bexplaining the true value of a variable, such as that included in the surface-obscure gray in Figure 7), which provides considerable assistance in developing applications and to understand the formulas of temporal logic [Ryb15]. From a practical point of view, contrary to the situation in the field of symbolic verification, for which a significant number of software are available (see [Ryb15]). For algorithms and implementation of parallel resolution, there is, to our knowledge, only one generic environment of Bresolution available for on− the− flyverification. It is Caesar[GLM18], a library for Balternation

resolution 1 created in using the Open / Caesarenvironment for on− the− flyverification. Caesarprovides an independent System of Boolean Equations B, in terms of Boolean graphs, the same way that Open / Caesarr provides

Illustrations are not included in the reading sample.

Figure 8: The result of distributed resolution on the flyof x1 with 3 nodes

a representation of States, independent of the language. Four algorithms are currently available in the library. A1 and A2 algorithms (they make no assumptions about the straight parts of B ), A2 performing diagnostics and optimization (examples and counter-examples). The A3 and A4 algorithms are specialized for the resolution in memory of acyclic system of Boolean Equations, which are frequently encountered in practice. The Caesar library is at the heart of several tools to check the CADPtoolbox [GLM18].

7. Research Methodology

7.1. Tasks definitions and distributed data

In distributed resolution of Boolean Equations System, each node is responsible for the exploration of a part of the Boolean graph. Fig. 8 shows the System of Boolean Equations given in Fig. 7 and distributes it over three nodes. The basic tasks of the resolution can be separated into:

7.1.1. a forward exploration (also known as expansion) of transitions of the Boolean graph (that is, dependencies between Boolean variables)

7.1.2. and secondly, a backwards propagation (also called stabilization)

Thus, the tasks executed on one node are independent and asynchronous with those performed on the other nodes. As a result, the various tasks required for the resolution of System of Boolean Equations can be efficiently distributed. Distributed data are vertices of the Boolean graph (that is, the Boolean variables of the system of Boolean equations). Note that, the type of exploration (depth first and chaotic, ...) of the Boolean graph, locally at a node, can globally affect the degree of parallelism of the distributed resolution of System of Boolean equations. Indeed, the set of data (that is, the portion of the Boolean graph) treated by a node depends on the order in which the vertices are crawled. It is constructed as the global exploration of the Boolean graph progresses. Thus, a Breadth First Search BFSwill favor the simultaneous construction on several nodes of a set of vertices of the Boolean graph to be explored, whereas a DFSwill construct and explore a single datum or vertexper node (this is the Boolean variable at the top of the stack of the deep path), which will generally result in processing the Boolean graph equivalently.

8. Implementation-DSOLVEalgorithm

We have implemented DSolvealgorithm in Cusing the Open / Caesarenvironment. Our algorithm is an integral part of the System of Boolean Equations Caesar-Solve Resolution Library [BDJM05], which has extensive documentation in the CADPdistribution. The user interface of DSolveis the same as that defined in this library. Thus, DSolvecan be used immediately by all CaesarSolve-based verification tools (eg.[BDJM05, GMLS07]). Finally, our implementation relies on the CaesarNetwork communication library, which provides the low layer (write / read of Tcp / Ip sockets) of transmissions and message rejections.

In order to test our DSolveimplementation, we have developed a Random System of Boolean equations that randomly produces an implicit System of Boolean equations (using a successor function which provides the transitions coming

Illustrations are not included in the reading sample.

Figure 9: Generation tool and random solution of System of Boolean Equations-mono bloc

Illustrations are not included in the reading sample.

Figure 10: DSolvealgorithm

out of a variable in the Boolean graph). Figure 9 shows the programming interface and execution environment of the System of Boolean equations-solver; obtained by connecting the Random System of Boolean equations generator and the DSolvealgorithm. It is the role of the supervisorto duplicate and run the executable programs on all nodes. The Random System of Boolean equations-solver provides a very accurate way of measuring DSolve’s performance, since the cost of calculating its successor function is negligible compared to the distributed resolution of System. In addition, an appropriate set of parameters allows the construction of a large variety of the system including those encountered in specific application domains, such as verification(comparison by Equivalences, evaluation of logical properties, partial order reduction) or the resolution of Horn clauses . The parameters used for class definition of the system are: the variable percentage of alternation type, that is, the proportion of variables; the percentage of Boolean constants in the System; the minimum and maximum number of variables; and the average length of a Boolean equation (branching factor of the Boolean graph). The Boolean variables (represented by integers) and their types (AND, OR) are randomly generated by means of a root.

8.1 DSOLVE algorithm

Our DSolvealgorithm for the System of Boolean equations is presented in Figure 10. This algorithm takes a Boolean graph G = (V, E, L) implicitly (ie. that is, by its successor function), an integer variable and x∈ V, a static hash function h: V→→→ [1, P], and the index iof the current node. DSolveperforms two interlaced paths of the Boolean graph, starting with the expansion of vertices of the Boolean graph and doing the stabilization of these vertices as soon

as possible. Once complete, the algorithm returns the Boolean value computed for x. After an initialization phase of the local data structures, the DSolvefunction loops until the resolution terminates. Each loop calculates one of the following three tasks, whose priority is given by cascading if− then− else expressions:

8.1.1. the expansion of unstable variables,

8.1.2. stabilization of variables by rear propagation , and

8.1.3. the receipt of messages from remote requests of stabilization or expansion requests.

9. Performance Analysis

To efficiently use the memory (since the workload is distributed among nodes by the static hash function), we assume that all the nodes are homogeneous in terms of Operating Systems (OS), processor and memory. Our experiments were mainly conducted on a 15 PcsXeon 2.4 GHz cluster with 1.5 GB Ram, running Linux, and interconnected by a gigabit network. We also did some experiments on a cluster of 216 Pcs Pentium III 733 MHz, with 256 MB of Ram, running Linux, mainly for scaling measurements. Finally, we used a local network of Sun workstations during development.

9.1. Acceleration and Effectiveness

Overall, the behavior of the equation algorithm is close to that of DSolvewith P= 1 which is also based on a DFS . Figure 11 shows the acceleration and efficiency obtained for three different classes of the System of Boolean Equations. Acceleration and efficiency are calculated on the basis of actual distributed resolution time, excluding the cost initiation phase. This cost is fixed and depend on the OS(copies of files, setting up communication channels, creating data structures).

One of the nodes is also used to execute the supervisorprocess in addition to the worker process. The re- sults shown in Figure 12 were obtained with Boolean Equations whose right side contained 10 variables on average, and a Bsize between 25, 104 and 107 variables. It should be noted that for each point on each curve, the System of Boolean Equations resolution has been executed ten times. The performance curves, like the acceleration in Figure 13, but also scaling in Figure 14 (left column) and memory consumption in Figure 15 (right column ), show the average of each set of ten executions excluding the minimum value and the maximum value. Figure 16 shows the System of Boolean Equations class on which DSolveachieves the best acceleration and efficiency.

This class is characterized by 0% alternation of variable type and 0% of Boolean constants. This class of Bcorresponds to the verification by equivalences (automatacomparison) when an automaton is deterministic(for the strong equivalence) and does not involve invisible transitions (for the weak equivalences) [Kei13] and the two automata are equivalent. Since no constant is present in the System of Boolean Equations, no stabilization occurs, and the resolution of the System is reduced to the exploration ahead of the whole Boolean graph.

It can be seen that acceleration and efficiency increase with the size of system and become super− linearfor problems of more than 2 variables. This can be explained by the fact that both DSolveand the equation algorithm use hash− tables (provided by the Open / Caesar environment) to store sets of Boolean variables.

Variables have a complexity in number of searches O(N/H), where His the number of entries (lists of collisions) of the hash table and Nis the number of variables in the table. From there, we update the hash tables during the execution of DSolveby (|E|/P)∆((|V|/P)/H) = (|E|∆(|V|/H))/P ² operations, assuming that the

set of dependencies Ehas also been divided into Punder a sub set, while it takes |E|∆(|V|/H) operations in the

sequential algorithm. This is why, for large System of Boolean Equations (ie, |V| >>H, for example, 6 · 10 ⁶ variables) and for a large number of nodes (split by a large P ² factor), our experiences can yield superlative results. The cost of updating the hash tables during equal solution becomes more important than the overhead of communication and buffermanagement of the distributed solution. We believe that similar behavior would occur with other data structures (for example, balancedsearch trees) used to manage sets of Boolean variables. Figure 16 represents a class of Bwith 100% alternation of variable type (that is, each −variablehas only −successors, and vice versa), and 10% Boolean constants. This class corresponds to the verification of non-deterministic systems (comparison by equivalence [Kri15] and partial order reduction [JM05]), and to the resolution of Horn clauses [FK17]. Acceleration and efficiency are slightly worse, since the Boolean constants cause some stabilization (and thus additional messages) during the first time. Thus, the overall communication cost in the distributed resolution is doubled, since each expansion message will most likely result in a stabilization message.

However, the backward− propagationof stable variables is limited because of 100% alternation parameter, which only propagates the stabilized variables to the immediate predictors ( for example, a stabilized −variableat Fwill not necessarily stabilize its −predecessors). Therefore, both equalization and distributed resolution have to explore most of the System, and the equalization is once again penalized when the System Bbecome very large (acceleration and efficiency become super− linear for Bexceeding 4 · 106 variables). Fig. 15 shows the class of the System of Boolean Equations with the lowest acceleration and efficiency results. The graph corresponds to Bwith alternating

Illustrations are not included in the reading sample.

Figure 11: Class (a) of the system of Boolean equations with 0% constants and 0% alternation

Illustrations are not included in the reading sample.

Figure 12: Class (b) of the system of Boolean equations with 10% constants and 100% alternation

variable type of 2% and 1% of Boolean constants. Such System, containing long paths of variables terminated by Fconstants, are often encountered in verification(comparison by equivalence of deterministic automataand evaluation of logical formulas [SEJK16]). The rearward spread of stable variables can be very fast and often reaches variables of interest. The equivalent algorithm implements an efficient propagation mechanism (since all the information on the predecessor dependencies is stored locally), whereas the communication via stabilization messages in DSolve( which are as numerous as expansion messages) can not be fully covered by computational activities. This inconvenience is barely visible when few nodes are used, but becomes important when many nodes are used on small systems. This explains the decrease in efficiency of DSolvewith this class of Bcompared to the previous System classes.

As with the previous System class, acceleration and efficiency become super−linearfor Bexceeding 4 · 106 variables.

We observe the same behavior for the system of Boolean Equations characterized by a percentage of alterna- tion of type of variables included in 0,100 and a percentage of Boolean constants in 0,100. More generally, for all classes of B, we observe that the greater the System, the better are the acceleration and the effectiveness made by DSolve.

This is also illustrated in Figures 12, 13 and 14. Another piece of information given by the efficiency curves is the trade-off between adding more nodes for computation and getting better acceleration. Thus, efficiency is also an indicator of DSolve’s good scaling, since most curves have a horizontal asymptotic properties.

Illustrations are not included in the reading sample.

Figure 13: Class (c) of the System of Boolean equations with 1% constants and 2% alternation

Illustrations are not included in the reading sample.

Figure 14: Class (a) of the System of Boolean equations with 0% const. and 0% alt.

Illustrations are not included in the reading sample.

Figure 15: Class (b) of the System of Boolean equations with 10% const. and 100% alt.

Illustrations are not included in the reading sample.

Figure 16: Class (c) of the system of Boolean equations with 1% const. and 2% alt.

10. Conclusion

V erificationof properties of parallel programs is an essential step in ensuring their smooth operation. For more than a decade, distributed verification has been proposed and recognized as a technique adapted to the problem of explosion verification. However, work on distributed verification has been moving in multiple directions. A large number of distributed algorithms have been defined, most of them are focusing on a specific aspect of the verification problem, for example load balancing or, on the contrary, the effectiveness of verification algorithms for a system written in a specific language. In addition, conflicting approaches (for example, the opposition of algorithms for distributed and shared memory architectures) have further accentuated the fragmented nature of the work in this area. In this study, we have used a pragmatic approach adapted to the needs of verification. This work focused on the design and construction of a generic infrastructure for model-based on distributed flight− testing , and its application to a number of different problems. The DSolve algorithm allowed an efficient distribution of the System of Boolean Equations resolution and computation on a set of interconnected machines. This is a cluster of PCs , while offering ease and efficiency of use in existing and new audit tools.

10.1. Future Works

The work presented in this research can be used in several directions. On the one hand, we can add features to our distributed algorithms so that they can handle a larger class of problems. On the other hand, it is possible to improve and extend the proposed on− the− fly audit tools and to build new ones according to the same schema. In order to increase its flexibility, the CaesarSolve 2 library can be enriched with other distributed System of Boolean Equations algorithms by developing distributed versions of algorithms such as Lmcor the algorithm based on Gauss− eliminationincluding equal equalization.

11. References

[Ace94] ACETO, Luca: A static view of localities. In: Formal Aspects of Computing6 (1994), Nr. 2, S. 201–222

[AV95] ANDERSEN, Henrik R. ; VERGAUWEN, Bart: Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In: International Conference on Computer Aided Verification Springer, 1995, S. 142–154

[BCM18] BASIN, David ; CREMERS, Cas ; MEADOWS, Catherine: Model checking security protocols. In:

Handbook of Model Checking. Springer, 2018, S. 727–762

[BDJM05] BERGAMINI, Damien ; DESCOUBES, Nicolas ; JOUBERT, Christophe ; MATEESCU, Radu: Bisimulator: A modular tool for on-the-fly equivalence checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems Springer, 2005, S. 581–585

[BL19] BISTRITZ, Ilai ; LESHEM, Amir: Game theoretic dynamic channel allocation for frequency-selective interference channels. In: IEEE Transactions on Information Theory65 (2019), Nr. 1, S. 330–353

[BT18] BARRETT, Clark ; TINELLI, Cesare: Satisfiability modulo theories. In: Handbook of Model Checking.

Springer, 2018, S. 305–343

[CDS00] CLEAVELAND, Rance ; DU, Xiaoqun ; SMOLKA, Scott A.: GCCS: A graphical coordination language for system specification. In: International Conference on Coordination Languages and Models Springer, 2000, S. 284–298

[CJGK⁺18] CLARKE JR, Edmund M. ; GRUMBERG, Orna ; KROENING, Daniel ; PELED, Doron ; VEITH, Helmut:

Model checking. MIT press, 2018

[Eas18] EASTMAN, Charles M.: Building product models: computer environments, supporting design and construction . CRC press, 2018

[Fer96] FERNANDEZ, Jean-Claude: Validation parévaluationsurunmodèle:méthodes et algorithmes, Université Joseph-Fourier-Grenoble I, Diss., 1996

[FK17] FU, Peng ; KOMENDANTSKAYA, Ekaterina: Operational semantics of resolution and productivity in Horn clause logic. In: Formal Aspects of Computing29 (2017), Nr. 3, S. 453–474

[GLM18] GARAVEL, Hubert ; LANG, Frédéric ; MOUNIER, Laurent: Compositional verification in action. In:

International Workshop on Formal Methods for Industrial Critical Systems Springer, 2018, S. 189–210

[GMJD12] GUINGO, Pierrick ; MOUILLERON, Vincent ; JANSEN, Arnold ; DAMM, Gerard: Distributed architecture for real-time flow measurement at the network domain level . Januar 10 2012. – US Patent 8,095,640

[GMLS07] GARAVEL, Hubert ; MATEESCU, Radu ; LANG, Frédéric ; SERWE, Wendelin: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: International Conference on Computer Aided Verification Springer, 2007, S. 158–163

[JKP19] JENSSEN, Matthew ; KEEVASH, Peter ; PERKINS, Will: Algorithms for# BIS-hard problems on expander graphs. In: Proceedings of the Thirtieth Annual ACM-SIAM Symposium on Discrete Algorithms Society for Industrial and Applied Mathematics, 2019, S. 2235–2247

[JM05] JOUBERT, Christophe ; MATEESCU, Radu: Distributed on-the-fly equivalence checking. In: Electronic Notes in Theoretical Computer Science 128 (2005), Nr. 3, S. 47–62

[JM06] JOUBERT, Christophe ; MATEESCU, Radu: Distributed on-the-fly model checking and test case generation.

In: International SPIN Workshop on Model Checking of SoftwareSpringer, 2006, S. 126–145

[Kei13] KEIREN, Jeroen Johan A.: Advanced reduction techniques for model checking. In: Eindhoven University of Technology (2013)

[Kri15] KRIOUILE, Abderahman: Formal Methods for Functional Verification of Cache-Coherent System-on-Chip,

Université Grenoble Alpes, Diss., 2015

[KYF⁺12] KIM, Eun A. ; YI, Jeong H. ; FOMIN, Alexey ; AFANASYEVA, Alexandria ; BEZZATEEV, Sergey: Method and system for performing distributed verification with respect to measurement data in sensor network .

August 28 2012. – US Patent 8,255,689

[Lam16] LAMPORT, Leslie: Specifying concurrent program modules. In: ACM Transactions on Programming Languages and systems (2016)

[Lar92] LARSEN, Kim G.: Efficient local correctness checking. In: International Conference on Computer Aided Verification Springer, 1992, S. 30–43

[LS98] LIU, Xinxin ; SMOLKA, Scott A.: Simple linear-time algorithms for minimal fixed points. In: International Colloquium on Automata, Languages, and Programming Springer, 1998, S. 53–66

[NKVL19] NGUYEN, Patrick An P. ; KRYZE, David ; VASSILAKIS, Theodore ; LERIOS, Apostolos: Systems and methods for a distributed query execution engine . Januar 8 2019. – US Patent App. 10/176,236

[RU19] RAMATCHANDIRANE, Nadaradjane ; UPADHYAY, Vandana: Program verification using hash chains.

Januar 22 2019. – US Patent App. 10/185,595

[Ryb15] RYBAKOV, Vladimir V.: Non-transitive linear temporal logic and logical knowledge operations. In:

Journal of Logic and Computation26 (2015), Nr. 3, S. 945–958

[SBF98] STUDER, Rudi ; BENJAMINS, V R. ; FENSEL, Dieter: Knowledge engineering: principles and methods.

In: Data & knowledge engineering25 (1998), Nr. 1-2, S. 161–197

[SEJK16] SICKERT, Salomon ; ESPARZA, Javier ; JAAX, Stefan ; KRˇ ETÍNSKY` , Jan: Limit-deterministic Büchi automata for linear temporal logic. In: InternationalConference on Computer Aided VerificationSpringer, 2016, S. 312–332

[Str04] STREJCEK, Jan: Linear temporal logic: Expressiveness and model checking , PhD thesis, Faculty of Informatics, Masaryk University in Brno, Diss., 2004

[SVA] SHKATOV, Dmitry ; VAN ALTEN, Clint J.: Complexity of the Universal Theory of Modal Algebras. In:

Studia Logica

[VSA19] VASAL, Deepanshu ; SINHA, Abhinav ; ANASTASOPOULOS, Achilleas: A systematic process for evaluating structured perfect Bayesian equilibria in dynamic games with asymmetric information. In:

IEEE Transactions on Automatic Control64 (2019), Nr. 1, S. 78–93

[YP19] YI, Peng ; PAVEL, Lacra: Distributed generalized Nash equilibria computation of monotone games via double-layer preconditioned proximal-point algorithms. In: IEEE Transactions on Control of Network Systems (2019)