Good morning,

Please, I used some design patterns in my IoT architecture. These patterns permit to ameliorate some quality attributes such as scalability, security, availability …

I need to know how to specify formally these quality attributes using Event-B method ?

Thank you for any suggestion or papers to recommend.

Cordially.