hrcak mascot   Srce   HID

Izvorni znanstveni članak
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

Puni tekst: engleski, pdf (1 MB) str. 1-16 preuzimanja: 37* citiraj
APA 6th Edition
Zahid, S., En-Nouaary, A. i Bah, S. (2019). Practical Model Checking of a Home Area Network System: Case Study. Journal of computing and information technology, 27 (2), 1-16. https://doi.org/10.20532/cit.2019.1004453
MLA 8th Edition
Zahid, Soufiane, et al. "Practical Model Checking of a Home Area Network System: Case Study." Journal of computing and information technology, vol. 27, br. 2, 2019, str. 1-16. https://doi.org/10.20532/cit.2019.1004453. Citirano 22.01.2020.
Chicago 17th Edition
Zahid, Soufiane, Abdeslam En-Nouaary i Slimane Bah. "Practical Model Checking of a Home Area Network System: Case Study." Journal of computing and information technology 27, br. 2 (2019): 1-16. https://doi.org/10.20532/cit.2019.1004453
Harvard
Zahid, S., En-Nouaary, A., i Bah, S. (2019). 'Practical Model Checking of a Home Area Network System: Case Study', Journal of computing and information technology, 27(2), str. 1-16. https://doi.org/10.20532/cit.2019.1004453
Vancouver
Zahid S, En-Nouaary A, Bah S. Practical Model Checking of a Home Area Network System: Case Study. Journal of computing and information technology [Internet]. 2019 [pristupljeno 22.01.2020.];27(2):1-16. https://doi.org/10.20532/cit.2019.1004453
IEEE
S. Zahid, A. En-Nouaary i S. Bah, "Practical Model Checking of a Home Area Network System: Case Study", Journal of computing and information technology, vol.27, br. 2, str. 1-16, 2019. [Online]. https://doi.org/10.20532/cit.2019.1004453

Sažetak
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.

Ključne riječi
Smart Grid, Promela generation, Formal modeling, V&V, SPIN, LTL

Hrčak ID: 228262

URI
https://hrcak.srce.hr/228262

Posjeta: 70 *