| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
A general approach to partial order reductions in symbolic verification
- 1998
-
Ingår i: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 379-390
-
Konferensbidrag (refereegranskat)abstract
- The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Handling Global Conditions in Parameterized System Verification
- 1999
-
Ingår i: Proc. 11th Int. Conf. on Computer Aided Verification. - Berlin : Springer Verlag. - 3540662022 ; , s. 134-145
-
Konferensbidrag (refereegranskat)abstract
- We consider symbolic verification for a class of parameterized systems, where a system consists of a linear array of processes, and where an action of a process may in general be guarded by both local conditions restricting the state of the process about to perform the action, and global conditions defining the context in which the action is enabled. Such actions are present, e.g., in idealized versions of mutual exclusion protocols, such as the bakery and ticket algorithms by Lamport, Burn’s protocol, Dijkstra’s algorithm, and Szymanski’s algorithm. The presence of both local and global conditions makes the parameterized versions of these protocols infeasible to analyze fully automatically, using existing model checking methods for parameterized systems. In all these methods the actions are guarded only by local conditions involving the states of a finite set of processes. We perform verification using a standard symbolic reachability algorithm enhanced by an operation to accelerate the search of the state space. The acceleration operation computes the effect of an arbitrary number of applications of an action, rather than a single application. This is crucial for convergence of the analysis e.g. when applying the algorithm to the above protocols. We illustrate the use of our method through an application to Szymanski’s algorithm.
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
On-the-fly analysis of systems with unbounded, lossy FIFO channels
- 1998
-
Ingår i: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 305-318
-
Konferensbidrag (refereegranskat)abstract
- 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 (i) computing 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 of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Simulation is decidable for one-counter nets
- 1998
-
Ingår i: CONCUR'98 Concurrency Theory. - 9783540648963 - 9783540684558 ; , s. 253-268
-
Konferensbidrag (refereegranskat)abstract
- We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of simulation preorder between pairs of processes in a class whose elements are neither finite-state nor allow finite partitioning of their state spaces.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Symbolic verification of lossy channel systems : Application to the bounded retransmission protocol
- 1999
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540657033 - 9783540490593 ; , s. 208-222
-
Konferensbidrag (refereegranskat)abstract
- We consider the problem of verifying automatically infinite- state systems that are systems of finite machines that communicate by exchanging messages through unbounded lossy fifo channels. In a previous work [1], we proposed an algorithmic approach based on constructing a symbolic representation of the set of reachable configurations of a system by means of a class of regular expressions (SREs). The construction of such a representation consists of an iterative computation with an acceleration technique which enhances the chance of convergence. This technique is based on the analysis of the effect of iterating control loops. In the work we present here, we experiment our approach and show how it can be effectively applied. For that, we developed a tool prototype based on the results in [1]. Using this tool, we provide an automatic verification of (the parameterized version of) the Bounded Retransmission Protocol.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Undecidable verification problems for programs with unreliable channels
- 1996
-
Ingår i: Automata, Languages and Programming. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540582014 - 9783540485667 ; , s. 71-90
-
Konferensbidrag (refereegranskat)abstract
- We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namelyThe model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.The results are obtained through a reduction from a variant of Post's Correspondence Problem.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verifying networks of timed processes
- 1998
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - 9783540643562 - 9783540697534 ; , s. 298-312
-
Konferensbidrag (refereegranskat)abstract
- Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.
|
|
| 8. |
|
|
| 9. |
- Kindahl, Mats, 1967-
(författare)
-
Verification of Infinite-State Systems : Decision Problems and Efficient Algorithms
- 1999
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- This thesis presents methods for the verification of distributed systems with infinite state spaces. We consider several verification problems for lossy channel systems, a class of infinite-state systems consisting of finite-state machines that communicate over unbounded, but lossy, FIFO channels. We also combine partial order techniques with symbolic techniques to improve performance of verification algorithms for infinite state systems.We study several implementation relations between lossy channel systems and finite transition systems, and show decidability of the following problems: trace inclusion, trace equivalence, simulation preorder, bisimulation equivalence, weak bisimulation equivalence in both directions, and weak simulation preorder in one direction. We further show that weak simulation preorder in the other direction is undecidable.Partial order reduction techniques are utilised to avoid exploring multiple interleavings of independent transitions. Constraint systems are introduced as a symbolic technique to represent (possibly infinite) sets of states. We present general methods for the application of partial order techniques for the verification of constraint systems. The method described is used for checking safety properties using forward or backward reachability analysis. It is based on the use of a—not necessarily symmetric—commutativity relation between operations. In contrast with previously existing approaches to partial order verification, which are based on a symmetric relation on transitions, our method does not require the relation to be symmetric. Partial order verification methods for lossy channel systems and for unsafe (i.e., infinite-state) Petri nets are developed to demonstrate the applicability of this approach.
|
|
