Khlifi, Oussama;  Mosbahi, Olfa; Khalgui, Mohamed; Frey, Georg; Li, Zhiwu: Modeling, Simulation and Verification of Probabilistic Reconfigurable Discrete-Event Systems under Energy and Memory Constraints. Iranian Journal of Science and Technology, Transactions of Electrical Engineering (2018).  [ACCEPTED].


Adaptive probabilistic systems have ability to modify their behaviors to cope with unpredictable significant changes at run-time such as component failures or resources depletion. Reconfiguration is often a major task for systems, i.e., it may violate the memory usage, the required energy and the concerned real-time constraints. It might also make the system's functions unavailable for some time and make potential harm to human life or large financial investments. Thus, updating a system with any new configuration requires that the post reconfigurable system fully satisfies the related constraints. Formal modeling and verification could avoid the resources and constraints violation. Thus, the paper proposes a new formalism to specify such systems. We also develop a new visual environment named ZIZO which helps in modeling, constructive simulation and CTL-based verification of adaptive probabilistic systems. The contributions are used to guarantee the resources and correctness of an IPv4 ZeroConf Protocol.