Jump to Content

Research areas

Distributed systems include notions of concurrency, communication, resource sharing and synchronisation. The Centre is concerned with distributed systems that can be considered discrete event systems. We thus use Coloured Petri Nets for modelling distributed systems as they possess well developed analysis techniques and their semi graphical nature facilitates visualisation of flow of control and data (or material). We also use automata theory (and labelled transition systems) to assist with analysis. Coloured Petri Nets are supported by well developed tools, Design/CPN and CPN Tools, which are used for most of the applications work. Timed Automata have been used in some applications. We are also investigating new analysis methods for Stochastic Petri Nets for improved performance analysis of distributed systems, and use TimeNET for experiments. For more information on Petri Nets in general, please visit Petri Nets World .

The research currently being undertaken by the Centre has five main thrusts: parametric verification, advanced reachability analysis algorithms, performance analysis, Internet protocols and Defence systems.  Research areas within these five thrusts include:

For details of specific projects being undertaken in these research areas, please see our Projects page. 

Parametric verification of computer network protocols

This research is aimed at developing techniques to analyse computer network systems and protocols where the need to consider system parameters leads to a large or infinite number of instantiations of the system to be analysed. This is often the case when the parameter values may be considered to be unbounded or unknown, e.g. maximum number of retransmissions, maximum sequence number and medium capacity. This work concentrates on developing explicit algebraic representations of classes of state spaces of such systems, and then developing symbolic analysis techniques to obtain general results. This is in contrast with the traditional approach of a separate analysis for each parameter value. This work is also useful when state space analysis is only possible for small values of the parameters due to the well known state explosion problem.

Funding

Researchers

Prof J. Billington, Dr Guy Gallasch, Dr Lin Liu, Mr Amar Gupta.

Collaborators

A/Prof Tomás Vojnar (Czech Republic), Mr Ales Smrcka (Czech Republic), Mr Andrey Rybalchenko (Germany).

Advanced reachability analysis algorithms

This research is concerned with developing new algorithms for the analysis of complex systems using state space approaches. This work concentrates on techniques for alleviating the state space explosion problem (such as equivalence classes and the sweep-line method) and their combinations. It involves local and international collaboration.

Funding

Australian Research Council Discovery Grants (2002-2004, 2005-2007).

Researchers

Prof J. Billington, Dr Guy Gallasch.

Collaborators

Prof Lars M. Kristensen (Norway), Dr Somsak Vanit-Anunchai (Thailand).

Performance Analysis using Generalised Stochastic Petri Nets

Performance analysis is important to determine properties such as throughputs and response times, allowing systems to be optimised. Unfortunately it is computationally expensive even for moderately large systems. This research aims to develop new aggregation techniques that significantly reduce computation time. We have developed an aggregation technique for state machine Generalised Stochastic Petri Nets (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. We are also using parametric techniques with this work. Outcomes include fundamental advances in performance analysis, new methodology and prototype tools.

Funding

ARC Discovery Grant, Aggregating Generalised Stochastic Petri Nets for Improved Performance Analysis, DP0880928, 2008-2010, $155K.

UniSA, Structural Aggregation of Generalised Stochastic Petri Nets for the Performance Analysis of Complex Systems, 2005, $25K.

Researchers

Prof J. Billington, A/Prof Kutlu Dogancay, Dr Guy Gallasch

Collaborators

Dr Joern Freiheit (Germany)

Internet protocols

Our modelling and analysis techniques are applied to Internet and related protocols that support the networking infrastructure required for advanced information services including e-commerce. Previous work in this area has investigated the Open Distributed Processing Trader, the Wireless Application Protocol (WAP), the Resource Reservation Protocol (RSVP), the Internet Open Trading Protocol (IOTP) and the Transmission Control Protocol (TCP). Current work includes investigations of multimedia control protocols (eg H.245 Capability Exchange Signalling Protocol), the Datagram Congestion Control Protocol (DCCP), mobile adhoc network protocols for route discovery (DYMO) and middleware interoperability (IIOP).

Funding

Researchers

Prof J. Billington, Dr Guy Gallasch, Dr Lin Liu, Ms Cong Yuan (PhD student), Mr Abhishek Singh (PhD student).

Collaborators

Dr Somsak Vanit-Anunchai (Thailand)

Agent protocols

We are currently investigating the verification of the Contract net protocol and its extensions for negotiating contracts between a company (auctioneer) and its subcontractors (bidders) with application to transport logistics. This work was stimulated by interaction with DSTO’s Command and Control Division at the end of 2006. It is currently investigating the use of parametric verification ideas, as the number of contractors (bidders) is a parameter of the system, and the use of equivalence classes.

Funding

UniSA, The Really Good Grants Scheme (ARC DP), Parametric Protocol Verification, 2009, $10K.

Researchers

Prof J. Billington, Mr Amar Gupta

Defence systems

The Centre has been involved with collaborative research with the Australian Defence Science and Technology Organisation (DSTO) for a decade. The projects have involved the application of coloured Petri nets to the modelling and analysis of avionics systems, operational planning, decision support systems and military logistics. A major project concerned the development of decision support systems for Operational Planning, in collaboration with DSTO and the Dynamic Planning, Optimisation and Learning Project (DPOLP) within National Information and Communications Technology Australia (NICTA). This work involved the development of a course of action scheduling tool (COAST) comprising a front end for planners and a back-end based on a Coloured Petri Net software package (CPN Tools). Our current work concerns the modelling and analysis of Defence Logistics and Maintenance processes, supported by the Land Operations Division of DSTO.

Funding

Researchers

Prof J. Billington, Dr Guy Gallasch.

High-level Petri Net Standards

This work is creating a multipart standard for High-level Petri nets. Part 1 on basic definitions using Universal Algebra was published in December 2004, and is currently in a revision cycle. Part 1 is been extended with an amendment on Symmetric Nets, a subclass of High-level nets which facilitates advanced reachability analysis using symmetries that can be calculated automatically. The work is close to finalisation, and will be incorporated into Part 1 during its revision. This work is related to our Parametric Verification research area. Part 2 is concerned with a transfer format for Petri nets and is close to finalisation. Part 3 on extensions (for modularity and timed aspects) is currently being discussed.

Funding

Internal and Standards Australia

Researchers

Prof J. Billington (overall ISO editor, and editor of Part 1).

top^