Skip to the main content

Original scientific paper

https://doi.org/10.20532/cit.2019.1004453

Practical Model Checking of a Home Area Network System: Case Study

Soufiane Zahid ; Institut National des Postes et Télécommunication, Rabat, Morocco
Abdeslam En-Nouaary ; Institut National des Postes et Télécommunication, Rabat, Morocco
Slimane Bah ; 2 Ecole Mohammadia d'Ingénieurs, University Mohammed V, Rabat, Morocco


Full text: english pdf 1.135 Kb

page 1-16

downloads: 380

cite


Abstract

The integrated communication infrastructure is the core of the Smart Grid architecture. Its two-way communication and information flow provides this network with all needed resources in order to control and manage all connected components from the utility to the customer side. This latter, named the Home Area Network or HAN, is a dedicated network connecting smart devices inside the customer home, and using different solutions. In order to avoid problems and anomalies along the process life cycle of developing a new solution for HAN network, the modeling and validation is one of the most powerful tools to achieve this goal. This paper presents a practical case study of such validation. It intends to validate a HAN SDL model, described in a previous work, using model checking techniques. It introduces a method to translate the SDL model to a Promela model using an intermediate format IF. After the generation of the Promela model, verification is performed to ensure that some functional properties are satisfied. The desired properties are defined in Linear Temporal Logic (LTL), and DTSPIN (an extension of SPIN with discrete time) model checker is used to verify the correctness of the model.

Keywords

Smart Grid; Promela generation; Formal modeling; V&V; SPIN; LTL

Hrčak ID:

228262

URI

https://hrcak.srce.hr/228262

Publication date:

18.11.2019.

Visits: 853 *