Application name:

Communications gateway using Coloured Petri Nets

Organisation:

University of South Australia (Defence Science and Technology Organisation)

Method:

Coloured Petri Nets

Tools:

Design/CPN; PROTEAN; Advanced Reachability Analysis (ARA)

Domain:

Gateway and protocol design

Period:

1994 - 1996

Size:

Initial specification: approximately 480 lines Refined specification: approximately 2100 lines.

Description:

The project investigated the use of Coloured Petri Nets and Design/CPN in the specification and partial implementation of a communications gateway.

Firstly a specification was developed using Design/CPN and its behaviour checked using its Occurrence Graph Analyser (OGA), looking for undesired behviour such as unwanted terminal states.

Then the specification was refined, adding functional entities and an internal protocol to map call control within the gateway. This refined specification was checked with the OGA tool. Once this test was complete the refined specification had to verified against the original specification. Language equivalence was chosen and PROTEAN was used to apply language reduction techniques to both CPN models.

The reduced languages were then compared using the ARA tool. Eventually the two models were found to be language equivalent.

Conclusions:

This project demonstated to us the benefits of carrying out formal analysis. Only after developing the refined specification and trying to equate it with the original specification, did we discover that the original specification was un-implementable. This fact would have been very hard to determine at the specification stage.

Publications:

D.Floreani, J.Billington, A.Dadej "Designing and Verifying a Communications Gateway using Coloured Petri Nets and Design/CPN",Proc 17th international Conference on the application and theory of Petri Nets, Osaka June 1996.

Contact:

Name:	Daniel Floreani
Organisation:	ITR
Address:	University of South Australia The Levels, South Australia
Country:	Australia
E-mail:	daniel@spri.levels.unisa.edu.au
Personal website:	http://www.itr.levels.edu.au/tsec/

URL:

http://www.itr.levels.edu.au/tsec/

© copyright 2004 | Formal Methods Europe