ZIZO is a Visual Environment for Modelling, Simulation and Formal Verification of Adaptive Probabilistic Discrete Event Control Systems Running Under Memory, Energy and Real-Time Constraints.


  • Model Systems Using the Formalism GR-TNCES (Generalized Reconfigurable Timed Net Condition/Event Systems),
  • Editing a model and connect modules with each other thanks to condition and event signals,
  • Choosing the simulation type according to probability level (high, average or low),
  • The simulation of the global model with a game token animation and a text trace 
  • Control simulation depending on memory and energy reserves and real-time evolution of reserve state: consumed as well as the memory and energy reserves,
  • Run the internal simulation of a single module,
  • Exporting the model to PRISM model checker by the generation of the model’s corresponding  Prism code  for the formal verification process,
  • Loading and saving model,
  • Perform some essential operation like: copy, cut, past, go to help, select an item, see model in tree view, delete selected module, free moving in work grid(go to top, bottom, left and right thanks to mouse wheel), zoom+, zoom-.


More Information

Contact: Oussama Khlifi

This Project is done in collaboration with LiSi LAB INSAT, Tunisia Polytechnic School: University of Carthage.
Responsible: Prof. Mohamed KHALGUI.