Details about ZIZO

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.

ZIZO Offer the Opportunity to:

  • 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-.

Fig.1: Modeling module of adaptive probabilistic discrete event system using GR-TNCES formalism.

Fig.2: Modeling distributed system and connection modules using event/condition signals.


Contact: Oussama Khlifi

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