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