Seite - 64 - in Intelligent Environments 2019 - Workshop Proceedings of the 15th International Conference on Intelligent Environments

Figure5. ThegeneratedUMLClassDiagramwith thecase study instances 5. ModelsGeneration 5.1. Methodology Here,wepresent theusedmethodology formodels generationandacase study to illus- trate theusabilityofourproposal.Weintendtogenerateastructuralpartandabehavioral part of a smart building system.Todo that,wefirst definemodel transformations from the smart buildingmetamodel (cf. Figure4) to aUMLClassDiagrammetamodel anda PetriNetsmetamodel inorder togenerate aUMLclassdiagramandaPetriNet respec- tivelly. To generate theUMLClassDiagram that represents the structural part,we rely on the transformation rules suchas:EClass toClass,Attribute toProperty,Supertype to Generalization,while the generationof thePetriNet that represents the behavioral part relies ondifferent rules related to the instantiated classes aswell as the chosenmodules andthedefinedconditionsandproperties.Transformationrulesareperformedwithin the Eclipse IDEwithAtlasTransformationLanguage (ATL). To generate a smart building system instance, we first create an instance from the smart buildingmetamodel. Then, by applying the transformation rules, we obtain the correspondingUMLClassDiagram, as shown inFigure 5,with only the necessary and instantiated classes alongwith the instances.We observe that the classesActuator and Variablearenot generated in themodel since theyarenot instantiated in the case study. Later, ifwechangeourcasestudybyaddinganactuator,wewillhaveageneratedUML Class Diagram containing theActuator class. By applying the transformation rules to PetriNets,weobtain thecorrespondingPetriNet as shown inFigure6. 5.2. Models validationandverification An important phase in our proposedmethodology is the validation and the verification of the system. The system structure (i.e., the generated UML Class Diagram) can be validatedwithin theEclipse IDE. The important task is to validate and formally verify the systembehavior (i.e. thegeneratedPetriNet) and thedesiredproperties (Safety and Liveness in our case study). To achieve this, we use TIme petri Net Analyzer (TINA) which is a toolbox for editing and analysis of Petri Nets. For that, we first performed A.LyazidiandS.Mouline /BuiS:AMethodology forSmartBuildingModeling64