:: Research Centre > Petri Nets for System Engineering Research Group

Home | Contact
 
Home
People
Collaborations
Projects
Publications
Important Links

 

Research Groups

   
Petri Nets for System Engineering Research Group (PSERG)
 

Petri Nets for System Engineering Group (PSERG) was formed to establish expertise and resources for research, development, and implementation of knowledge-based software systems in Faculty of Information Technology at University of Central Punjab, Lahore, Pakistan.

We conduct research on many aspects of System Engineering & Petri Nets based Modeling with an emphasis on the algorithmic aspects of problems.

Why Formal Methods?
Formal methods are techniques used to model complex systems as mathematical entities. By building a mathematically rigorous model of a complex system, it is possible to verify the system's properties in a more thorough fashion than empirical testing.

What is a Petri Net?
Petri Nets is a formal and graphical appealing language which is appropriate for modelling systems with concurrency. Petri Nets has been under development since the beginning of the 60'ies, where Carl Adam Petri defined the language. It was the first time a general theory for discrete parallel systems was formulated. The language is a generalization of automata theory such that the concept of concurrently occurring events can be expressed. Petri Nets can be used to model a wide range of various systems.

Why Coloured Petri Net?
Coloured Petri Nets (CPNs) are an extension of ordinary Petri Nets. CPNs provide a modeling framework suitable for simulating distributed and concurrent processes with both synchronous and asynchronous communication. They are useful in modeling both nondeterministic and stochastic processes as well. CPNs extend the vocabulary of ordinary Petri Nets and add features that make them suitable for modeling large systems. CPNs combine the strengths of ordinary Petri Nets with the strengths of a high-level programming language called CPN ML which is based on the functional language SML (Ullman 1998). Petri Nets provide the primitives for process interaction, while the programming language provides the primitives for the definition of data types and the manipulations of data values.

What is CPN Tools?
CPN Tools has an intuitive graphical user interface that is useful for editing, simulating, and analyzing Colored Petri nets. The tool features incremental syntax checking and code generation, which take place while a net is being constructed. CPNs provide a unified approach for analysis of both functional/logical properties as well as performance properties through their support for both timed and untimed activities within a single formalism. Thus one does not have to create two separate models to carry out such analyses. Furthermore, unlike many discrete event simulation systems, CPNs provide a set of state space methods for verification of system properties. The state space approach complements analysis that can be performed based on pure simulation. CPNs support a mechanism of modules for construction of large system models in a hierarchical manner. The hierarchy and module concept of CPNs permit different levels of abstraction that are inherent in most complex systems. The graphical representation makes it easy to see the basic structure of a complex CPN model and understand the interaction of individual sub-components.

Net Models:

  • Extended Ordinary Petri Nets.
  • Coloured Petri Nets.
  • Timed Petri Nets.
  • Fuzzy Petri Nets.
  • Hierarchical Timed Petri Nets.
  • Stochastic Petri nets

Research Areas in Petri Nets:

  • Formal specification and verification of Real-time Systems via Petri Nets.
  • Timed Petri-nets-based scheduling approach.
  • Algorithms Designing and Formalizing, Proving Techniques, Model Checking
  • Petri-nets-based methodology for batch processes
  • Application to manufacturing systems and industrial processes
  • Reachability analysis; modeling and analysis of concurrent software
  • Applications in command and control systems.
  • Verification through Model-Checking  for Wireless Mobile Ad Hoc Networks
  • Design Methodology, Validation and verification of Wireless Mesh Networks.
  • Stochastic process solution techniques
  • Network protocols designing and verification.
  • Modular reasoning and abstraction techniques for model checking

 

University of Central Punjab