Modeling, Simulation and Verification of Probabilistic Reconfigurable Discrete-Event Systems Under Energy and Memory Constraints

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.