Formal Modelling and Verification

The Formal Modelling and Verification Group is active in the the following areas:

Modelling Concurrent Systems (Theoretical Issues)
• Petri Nets
• Communicating Sequential Processes
• Modelling and verification of heterogeneous systems
  • Language and semantic support for systems level design
  • Representation of functional and constraint information
  • Component based verification of dataflow process networks
  Analysis of Concurrent Systems (Tool issues)
• Petri net reachability and invariant analysis of specifications utilising references and refinement
• Model/refinement checking
• Simulation, animation and model checking of heterogeneous systems