Detecting Anti-Pattern in Event-B

Nowadays generate reliable patterns is a challenge in the software engineering field, so anti-patterns detection becomes an effective and objective concept to be sure of the correctness of the software. Detecting anti-patterns early in the design level will be a good chance to avoid greater losses in cost and time. Many problems will be avoided also. In our thesis we discuss these two types of informal problems on Insulin Infusion Pump (IIP) .The proposed approach to formalize IIP is based on using Event-B. Finally, we could verify that the code generated from the proposed approach is correct and formal to use as a pattern. The accuracy of the proposed verification steps are suitable for using to any systems or medical device. The method ameliorates the proof percentage.