| 1. |
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- Abdulla, Aziz, et al.
(författare)
-
Monotonic Abstraction : on Efficient Verification of Parameterized Systems
- 2009
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:5, s. 779-801
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols
|
|
| 5. |
|
|
| 6. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
A classification of the expressive power of well-structured transition systems
- 2011
-
Ingår i: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 209:3, s. 248-279
-
Tidskriftsartikel (refereegranskat)abstract
- We compare the expressive power of a class of well-structured transition systems that includes relational automata (extensions of), Petri nets, lossy channel systems, constrained multiset rewriting systems, and data nets. For each one of these models we study the class of languages generated by labeled transition systems describing their semantics. We consider here two types of accepting conditions: coverability and reachability of a fixed a priori configuration. In both cases we obtain a strict hierarchy in which constrained multiset rewriting systems is the most expressive model.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Automatic verification of directory-based consistency protocols with graph constraints
- 2011
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 761-782
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Constrained monotonic abstraction : A CEGAR for parameterized verification
- 2010
-
Ingår i: CONCUR 2010 – Concurrency Theory. - Berlin : Springer-Verlag. - 9783642153747 ; , s. 86-101
-
Konferensbidrag (refereegranskat)abstract
- In this paper, we develop a counterexample-guided abstraction refinement (CEGAR) framework for monotonic abstraction, an approach that is particularly useful in automatic verification of safety properties for parameterized systems The main drawback of verification using monotonic abstraction is that it sometimes generates spurious counterexamples Our CEGAR algorithm automatically extracts from each spurious counterexample a set of configurations called a "Safety Zone" and uses it to refine the abstract transition system of the next iteration We have developed a prototype based on this idea, and our experimentation shows that the approach allows to verify many of the examples that cannot be handled by the original monotonic abstraction approach.
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Handling parameterized systems with non-atomic global conditions
- 2008
-
Ingår i: Verification, Model Checking, and Abstract Interpretation. - Berlin : Springer-Verlag. ; , s. 22-36
-
Konferensbidrag (refereegranskat)abstract
- We consider verification of safety properties for parameterized systems with linear topologies. A process in the system is an extended automaton, where the transitions are guarded by both local and global conditions. The global conditions are non-atomic, i.e., a process allows arbitrary interleavings with other transitions white checking the states of all (or some) of the other processes. We translate the problem into model checking of infinite transition systems where each configuration is a labeled finite graph. We derive an over-approximation of the induced transition system, which leads to a symbolic scheme for analyzing safety properties. We have implemented a prototype and run it on several nontrivial case studies, namely non-atomic versions of Burn's protocol, Dijkstra's protocol, the Bakery algorithm, Lamport's distributed mutual exclusion protocol, and a two-phase commit protocol used for handling transactions in distributed systems. As far as we know, these protocols have not previously been verified in a fully automated framework.
|
|
| 10. |
|
|
