MOGEVE

MOdel, Generate Event-B specification and Verify self-adaptive systems MOGEVE is a plugin eclipse that enables building design patterns-based self-adaptive WSN applications. In this framework, we propose (i) a self-adaptive design patterns (centralized, distributed and hybrid) based on IBM MAPE control loop (Monitor, Analyze, Plan and Execute), (ii) a UML profile that assists software architects to design their self-adaptive WSN applications while following these patterns, and (iii) a formal checking of theses designed applications with an automatic transfor-mation of their UML designs to Event-B specifications. The proposed solution offers a consistent, reusable, and flexible specification of the adaptation activities thanks to the design pattern and the formal proving.it is composed ofa graphical modeling tool that ensures an easy and efficient modeling way of MAPE design patterns and their formal specification.