1541. |
- 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.
|
|
1542. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
On the verification of timed ad hoc networks
- 2011
-
Ingår i: Formal Modeling and Analysis of Timed Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642243097 ; , s. 256-270
-
Konferensbidrag (refereegranskat)
|
|
1543. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized tree systems
- 2008
-
Ingår i: Formal Techniques for Networked and Distributed Systems. - Berlin : Springer-Verlag. - 9783540688549 ; , s. 69-83
-
Konferensbidrag (refereegranskat)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.
|
|
1544. |
- Abdulla, Parosh A., et al.
(författare)
-
Parameterized verification
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 469-473
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)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.
|
|
1545. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification of time-sensitive models of ad hoc network protocols
- 2016
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 612, s. 1-22
-
Tidskriftsartikel (refereegranskat)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.
|
|
1546. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification through view abstraction
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 495-516
-
Tidskriftsartikel (refereegranskat)abstract
- We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
|
|
1547. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
Parameterized verification under TSO is PSPACE-complete
- 2020
-
Ingår i: Proceedings of the ACM on Programming Languages. - New York, NY, USA : Association for Computing Machinery (ACM). - 2475-1421. ; 4:POPL, s. 26:1-26:29
-
Tidskriftsartikel (refereegranskat)abstract
- We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
|
|
1548. |
|
|
1549. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Precise and sound automatic fence insertion procedure under PSO
- 2015
-
Ingår i: Networked Systems. - Cham : Springer. - 9783319268491 ; , s. 32-47
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete procedure for fence insertion for concurrent finite-state programs running under the PSO memory model. This model allows ''write to read'' and ''write-to-write'' relaxations corresponding to the addition of an unbounded store buffers between processors and the main memory. We introduce a novel machine model, called the Hierarchical Single-Buffer (HSB) semantics, and show that the reachability problem for a program under PSO can be reduced to the reachability problem under HSB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure infers automatically a minimal set of fences that ensure correctness of the program. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples.
|
|
1550. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Priced timed Petri nets
- 2013
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 9:4, s. 10:1-51
-
Tidskriftsartikel (refereegranskat)
|
|