Petri net analyser - project description

Supervisor: William J. Knottenbelt <wjk>
Room No.: 371 Huxley

Details at:

Petri nets are a popular graphical way of modelling concurrent systems such as communications protocols, multiprocessor computers etc. With Petri nets it is possible to assess the correctness of systems - for example by verifying that the system cannot deadlock, that there cannot be any buffer overflows etc. Stochastic Petri nets extend ordinary Petri nets by incorporating time. This allows designers to use the same formalism to reason both about the correctness and the performance of systems.

Although there are many Petri net tools available (click here for a list of about 100 such tools), their functionality is limited to that which their programmers provide at the time of writing. Your task is to construct a modular Petri net editor/animator that supports the arbritary run-time extension of its analysis power by user-designed modules. Examples of modules you might like to write to illustrate the power of this framework is a module which integrates with an existing Markov chain performance analyser to produce performance statistics (such as the throughput of a data communication protocol), a corresponding module which produces the same statistics except by simulation, an invariant analysis module which deduces correctness properties from the structure of the Petri net, a response time analysis module etc. etc. Can you go even further and make components of the editor pluggable, so that the tool can be extended to support new Petri net types with minimal effort?

So that it is portable, the tool should be written in Java using the Swing graphics library. You will also be using the latest XML Petri net standards to represent your nets. This means you should have some Java/C++/Object-oriented design experience. However, no previous knowledge of Petri nets or analytical performance analysis techniques is necessary.

Click here for background material about modelling systems with Petri nets.