ARC Discovery Grant Projects (2002-2010)
- Aggregating Generalised Stochastic Petri Nets for Improved Performance Analysis (2008-2010)
- Advances in the Verification of Communication Protocols (2005-2007)
- Advanced Sweepline State Space Reduction Methods for Verification of Concurrent and Distributed Systems (2002-2004)
Aggregating Generalised Stochastic Petri Nets for Improved Performance Analysis
This project aims to develop new aggregation techniques for Generalised Stochastic Petri Nets (GSPNs) that significantly reduce computation time. We have developed an aggregation technique for state machine GSPNs, which dramatically reduces computation time and leads to closed form solutions. We intend to extend this technique to a richer class of GSPNs so that a broader range of systems can be analysed. Outcomes include fundamental advances in performance analysis, new methodology and prototype tools.
The project is funded by an Australian Research Council Discovery Grant (2008-2010).
Advances in the Verification of Communication Protocols
The aim of this project is to discover efficient analysis techniques for the verification of network protocols. Network protocols nearly always include parameters, such as: the maximum number of retransmissions; the maximum sequence number; window sizes for flow control and congestion control; and medium capacity. Parameters may require a large or infinite number of instantiations of the system to be analysed, and hence their verification is a challenging problem. This work concentrates on deriving algebraic representations of classes of state spaces of such systems, based on recognising patterns in state spaces as the parameter values are increased. We have obtained results for a number of different case studies including TCP's Data Transfer Service, the Capability Exchange Signalling Protocol and Service (a multimedia control protocol standardized by the International Telecommunications Union) and credit-based flow control protocols (including the stop-and-wait class of protocols). The project also tackles the problem of whether these techniques carry through to the automata representing protocol and service languages, to enable their comparison for verification at the symbolic level.
The project is funded by an Australian Research Council Discovery Grant (2005-2007).
Advanced Sweepline State Space Reduction Methods for Verification of Concurrent and Distributed Systems
The rigorous design and analysis of distributed systems, such as the Internet and its applications, is known to be a difficult problem. This project aims to develop new techniques for reducing the memory and time required for computer-aided verification of concurrent and distributed systems, in particular, the Sweep-Line State Space Reduction method. This technique will be combined with other reduction techniques to increase their range of applicability.
The reduction techniques will be implemented and evaluated using important transaction protocols including Internet enabled wireless communications. The technique will also be applied to object oriented modelling languages.
This work is carried out as a joint project with Adelaide University and the University of Aarhus, Denmark. It is supported by an Australian Research Council (ARC) Discovery Grant (2002-2004).