| 1. |
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Better-Structured Transition Systems
- 2004
-
Reports (other academic/artistic)abstract
- In automated verification of infinite-state systems, a variety of algorithms that operate on constraints representing sets of states have been developed. Many of these algorithms rely on well quasi-ordering of the constraint system for proving termination. A number of methods for generating new well quasi-ordered constraint systems have been proposed. However, many of these constraint systems suffer from constraint explosion as the number of constraints generated during analysis grows exponentially with the size of the problem. We suggest using the theory of better quasi-ordering to prove termination since that will allow generation of constraint systems that are less prone to constraint explosion. We also present a method to derive such constraint systems. We introduce existential zones, a constraint system for verification of systems with an unbounded number of clocks and use our methodology to prove that existential zones are better quasi-ordered. We show how to use existential zones in verification of timed Petri nets and present some experimental results. Finally, we present several other constraint systems which have been derived using our methodology.
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(author)
-
BQOs and Timed Petri Nets
- 2000
-
Reports (other academic/artistic)abstract
- In this paper, we use the theory of better quasi-orderings to define a methodology for inventing constraint systems which are both well quasi-ordered and compact. We apply our methodology by presenting new constraint systems for verification of systems with unboundedly many real-valued clocks, and use them for checking safety properties for lazy (non-urgent) timed Petri nets where each token is equipped with a real-valued clock.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Downward Closed Language Generators
- 2003
-
Reports (other academic/artistic)abstract
- We use downward closed languages for representing sets of states when performing forward reachability analysis on infinite-state systems. Downward closed languages are often more succinct than exact representations of the set of reachable states. We introduce a formalism for representing downward closed languages, called downward closed language generators (dlgs). We show that standard set operations needed for performing symbolic reachability analysis are computable for dlgs. Using a class of hierarchically defined dlgs, we have implemented a prototype for analysing timed Petri nets and used it to analyze a parameterized version of Fischer's protocol. We also show how dlgs can be used for uniform representation of formalisms previously presented for models such as Petri nets and lossy channel systems.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Forward Reachability Analysis of Timed Petri Nets
- 2003
-
Reports (other academic/artistic)abstract
- We consider verification of safety properties for concurrent real-timed systems modelled by timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions. Downward closed languages provide exact abstractions of sets of reachable states with respect to safety properties.We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples.We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol. We also used the tool to generate a finite-state abstraction of the protocol.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Timed Petri Nets and BQOs
- 2001
-
In: Proc. 22nd Int. Conf. on Application and Theory of Petri Nets 2001. - : Springer Verlag. ; , s. 53-70
-
Conference paper (peer-reviewed)
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Unfoldings of Unbounded Petri Nets
- 2000
-
In: Proc. 12tn Int. Conf. on Computer Aided Verification. - : Springer Verlag. ; , s. 495-507
-
Conference paper (peer-reviewed)
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Using Forward Reachability Analysis for Verification of Timed Petri Nets
- 2007
-
In: Nordic Journal of Computing. - 1236-6064. ; 14:1, s. 1-42
-
Journal article (peer-reviewed)abstract
- We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol, Lynch and Shavit's mutual exclusion protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.
|
|
| 9. |
|
|
| 10. |
|
|
