Using BECAMEDA method to specify and verify a smart home system

Designing a correct model for smart systems requires an accurate specification and verification prior to development. This paper proposes the use of BECAMEDA (Behavioral SpEcification and VerifiCAtion of RMAS based on E-MDRA) method, which helps the designer predicting the system behaviour, and verifying the relevant behaviour of the system properties. BECAMEDA method is based on Multi-Agent concept and formal method, and it proposes an iterative process consisted of four phases: identification, definition, modelling and verification, to help understanding the system starting from goals identification that captures the system needs, and ending with a formal verification of the system properties. The proposed method is illustrated with an example of a Smart Home System1.