| 1. |
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
- Abdulla, Aziz, et al.
(author)
-
Monotonic Abstraction : on Efficient Verification of Parameterized Systems
- 2009
-
In: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:5, s. 779-801
-
Journal article (peer-reviewed)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.
(author)
-
A classification of the expressive power of well-structured transition systems
- 2011
-
In: Information and Computation. - : Elsevier BV. - 0890-5401 .- 1090-2651. ; 209:3, s. 248-279
-
Journal article (peer-reviewed)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.
(author)
-
Automatic verification of directory-based consistency protocols with graph constraints
- 2011
-
In: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 761-782
-
Journal article (peer-reviewed)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.
(author)
-
Constrained monotonic abstraction : A CEGAR for parameterized verification
- 2010
-
In: CONCUR 2010 – Concurrency Theory. - Berlin : Springer-Verlag. - 9783642153747 ; , s. 86-101
-
Conference paper (peer-reviewed)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.
(author)
-
Handling parameterized systems with non-atomic global conditions
- 2008
-
In: Verification, Model Checking, and Abstract Interpretation. - Berlin : Springer-Verlag. ; , s. 22-36
-
Conference paper (peer-reviewed)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. |
|
|
| 11. |
- Abdulla, Parosh Aziz, et al.
(author)
-
On the verification of timed ad hoc networks
- 2011
-
In: Formal Modeling and Analysis of Timed Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642243097 ; , s. 256-270
-
Conference paper (peer-reviewed)
|
|
| 12. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Parameterized tree systems
- 2008
-
In: Formal Techniques for Networked and Distributed Systems. - Berlin : Springer-Verlag. - 9783540688549 ; , s. 69-83
-
Conference paper (peer-reviewed)abstract
- Several recent works have considered parameterized verification, i.e. automatic verification of systems consisting of an arbitrary number of finite-state processes organized in a linear array. The aim of this paper is to extend these works by giving a simple and efficient method to prove safety properties for systems with tree-like architectures. A process in the system is a finite-state automaton and a transition is performed jointly by a process and its parent and children processes. The method derives an over-approximation of the induced transition system, which allows the use of finite trees as symbolic representations of infinite sets of configurations. Compared to traditional methods for parameterized verification of systems with tree topologies, our method does not require the manipulation of tree transducers, hence its simplicity and efficiency. We have implemented a prototype which works well on several nontrivial tree-based protocols.
|
|
| 13. |
- Abdulla, Parosh A., et al.
(author)
-
Parameterized verification
- 2016
-
In: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 469-473
-
Journal article (other academic/artistic)abstract
- The goal of parameterized verification is to prove the correctness of a system specification regardless of the number of its components. The problem is of interest in several different areas: verification of hardware design, multithreaded programs, distributed systems, and communication protocols. The problem is undecidable in general. Solutions for restricted classes of systems and properties have been studied in areas like theorem proving, model checking, automata and logic, process algebra, and constraint solving. In this introduction to the special issue, dedicated to a selection of works from the Parameterized Verification workshop PV '14 and PV '15, we survey some of the works developed in this research area.
|
|
| 14. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Parameterized verification of time-sensitive models of ad hoc network protocols
- 2016
-
In: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 612, s. 1-22
-
Journal article (peer-reviewed)abstract
- We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.
|
|
| 15. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Push-down automata with gap-order constraints
- 2013
-
In: Fundamentals of Software Engineering. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642402128 ; , s. 199-216
-
Conference paper (peer-reviewed)
|
|
| 16. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Regular Model Checking without Transducers
- 2007
-
In: TACAS'07, The 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.
-
Conference paper (peer-reviewed)
|
|
| 17. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Regular Model Checking without Transducers (On Efficient Verification of Parameterized Systems)
- 2006
-
Reports (other academic/artistic)abstract
- We give a simple and efficient method 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. The method derives an over-approximation of the induced transition system, which 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 which works well on several mutual exclusion algorithms and cache coherence protocols.
|
|
| 18. |
- Abdulla, Parosh A., et al.
(author)
-
Well Structured Transition Systems with History
- 2015
-
In: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; :193, s. 115-128
-
Journal article (peer-reviewed)abstract
- We propose a formal model of concurrent systems in which the history of a computation is explicitly represented as a collection of events that provide a view of a sequence of configurations. In our model events generated by transitions become part of the system configurations leading to operational semantics with historical data. This model allows us to formalize what is usually done in symbolic verification algorithms. Indeed, search algorithms often use meta-information, e.g., names of fired transitions, selected processes, etc., to reconstruct (error) traces from symbolic state exploration. The other interesting point of the proposed model is related to a possible new application of the theory of well-structured transition systems (wsts). In our setting wsts theory can be applied to formally extend the class of properties that can be verified using coverability to take into consideration (ordered and unordered) historical data. This can be done by using different types of representation of collections of events and by combining them with wsts by using closure properties of well-quasi orderings.
|
|
| 19. |
- Abdulla, Parosh, et al.
(author)
-
Handling Parameterized Systems with Non-Atomic Global Conditions
- 2007
-
Reports (other academic/artistic)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 while 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.
|
|
| 20. |
- Abdulla, Parosh, Professor, 1961-, et al.
(author)
-
On the Formalization of Decentralized Contact Tracing Protocols
- 2020
-
In: Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 {(BOSK} 2020), September 25, 2020. - : CEUR-WS.org. ; , s. 65-70
-
Conference paper (peer-reviewed)abstract
- We present a preliminary formalization based on transition systems of decentralized contact tracing protocols for smart devices equipped with Bluetooth trasmitters. In our model the behaviour of individual users, via their app, is modelled as a timed automata with a local unbounded memory. Protocol configurations consist of the current state of a shared server and a finite set of local states containing the states of individual users. The transition system models the interaction between devices in the same physical location and between a sigle device and the shared server. In the paper we address different research directions concerning semi-automated verification based on automated reasoning tools of the considered class of protocols, theoretical issues related to the expressiveness of the resulting class of formal models, and data-driven analysis of the logs collected on the server as well as on user devices.
|
|
| 21. |
- Abdulla, Parosh, et al.
(author)
-
Parameterized Verification of Infinite-state Processes with Global Conditions
- 2007
-
In: Computer Aided Verification, Proceedings. - : Department of Information Technology, Uppsala University. - 9783540733676 ; , s. 145-157
-
Conference paper (peer-reviewed)abstract
- We present a simple and effective approximated backward reachability algorithm for parameterized systems with existentially and universally quantified global conditions. The individual processes operate on unbounded local variables ranging over the natural numbers. In addition, processes may communicate via broadcast, rendez-vous and shared variables. We apply the algorithm to verify mutual exclusion for complex protocols such as Lamport's bakery algorithm both with and without atomicity conditions, a distributed version of the bakery algorithm, and Ricart-Agrawala's distributed mutual exclusion algorithm.
|
|
| 22. |
- Delzanno, Giorgio, et al.
(author)
-
A lightweight regular model checking approach for parameterized systems
- 2012
-
In: International Journal on Software Tools for Technology Transfer. - : Springer-Verlag New York. - 1433-2779 .- 1433-2787. ; 14:2, s. 207-222
-
Journal article (peer-reviewed)abstract
- In recent years, we have designed a lightweight approach to regular model checking specifically designed for parameterized systems with global conditions. Our approach combines the strength of regular languages, used for representing infinite sets of configurations, with symbolic model checking and approximations. In this paper, we give a uniform presentation of several variations of a symbolic backward reachability scheme in which different classes of regular expressions are used in place of BDDs. The classification of the proposed methods is based on the precision of the resulting approximated analysis.
|
|
