Page - 65 - in Intelligent Environments 2019 - Workshop Proceedings of the 15th International Conference on Intelligent Environments

Figure6. ThegeneratedPetriNet another transformation from the generated PetriNetmodel to a textual PetriNet (.tpn) conformstoTINA.Then,byreadingthe .tpnfilewithinTINA,wecancheckthenetsyn- tax and also perform the necessary analysis (Structural andReachability). The toolbox indicate that the syntaxcheck is successful.Furthermore, byperformingstructural anal- ysisandreachabilityanalysis,weobserve that thenet isboundedandlive(nodeadlocks) meaning that theSafetyproperty is satisfied.Also, noplacenor transition is dead in the generatednetmeaning that theLivenessproperty is satisfied. 6. Conclusions In this paper, we intend to improve one of themost used environments, buildings. For that,wefirst definea smart building systemarchitecture.Then,wepresent ourmethod- ology for smart building design and implementation. Finally,we perform anMDEap- proach to generate smart building system models and perform the necessary analysis in order to validate and formally verify the system. In the future, we aim to develop a framework including a specificmodeling language for smart buildingwhichwill allow morebehaviormodelingandwill includeanautomaticvalidationandverificationphase. References [1] H.Chen, P.Chou, S.Duri,H.Lei and J.Reason, ”Thedesign and implementation of a smart building control system”, In e-Business Engineering, 2009. ICEBE’09. IEEE International Conference on (pp. 255-262). IEEE,2009. [2] D. Sciuto and A. A. Nacci, ”On how to design smart energy-efficient buildings”, In Embedded and UbiquitousComputing (EUC),201412th IEEEInternationalConferenceon(pp.205-208). IEEE,2014 [3] S. Lazarova-Molnar, H. R. Shaker andN.Mohamed, ”Fault detection and diagnosis for smart build- ings: State of the art, trends and challenges”, InBigData and Smart City (ICBDSC), 2016 3rdMEC InternationalConferenceon (pp.1-7), IEEE,2016. [4] T.G.Stavropoulos,D.Vrakas,D.VlachavaandN.Bassiliades,”BOnSAI:asmartbuildingontologyfor ambient intelligence”, In Proceedings of the 2nd international conference onweb intelligence,mining andsemantics (p.30),ACM,2012. [5] K. Fra¨mling, I.Oliver, J.Honkola, and J.Nyman, ”Smart spaces for ubiquitously smart buildings”, In 2009Third International Conference onMobileUbiquitous Computing, Systems, Services and Tech- nologies (pp.295-300), 2009. [6] O.Evangelatos,K.Samarasinghe and J.Rolim, ”Evaluatingdesign approaches for smart building sys- tems”, InMobileAdhocandSensorSystems, IEEE9th InternationalConferenceon (pp.1-7), 2012. [7] B.L.ThomasandD.J.Cook,”Activity-awareenergy-efficientautomationofsmartbuildings”,Energies, 9 (2016), 624. [8] S.Wang, ”Intelligentbuildingsandbuildingautomation”,Routledge,2009. [9] A.Lyazidi, andS.Mouline, ”Ametamodel-driven definition and implementation ofONDAR: a home automationontology”, Int. J.ComputerApplications inTechnology,58 (2018), 198–210. A.LyazidiandS.Mouline /BuiS:AMethodology forSmartBuildingModeling 65