| 1. |
- 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.
|
|
| 2. |
- Abdulla, Parosh Aziz, Professor, et al.
(författare)
-
Model checking parameterized systems
- 2018
-
Ingår i: Handbook of Model Checking. - Cham : Springer. - 9783319105741 ; , s. 685-725
-
Bokkapitel (refereegranskat)
|
|
| 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 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.
|
|
| 5. |
- Abdulla, Parosh A., et al.
(författare)
-
Well Structured Transition Systems with History
- 2015
-
Ingår i: Electronic Proceedings in Theoretical Computer Science. - 2075-2180. ; :193, s. 115-128
-
Tidskriftsartikel (refereegranskat)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.
|
|
| 6. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Parameterized Verification under TSO with Data Types
- 2023
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Paris, France, April 22-27, 2023, Proceedings, Part {I}. - 9783031308239 ; , s. 588-606
-
Konferensbidrag (refereegranskat)
|
|
