در اين تحقيق با استفاده از زبان فرمال شبكه هاي پتري، از بخش ها و جنبه هاي مختلف لايه مجازي سازي در ديتا سنترها، مدل هاي فرمال متعددي تهيه شده است. سپس به كمك ابزار رياضي، رفتار اين مكانيزم ها براي تعيين سطح خوش رفتاري سيستم بررسي شده است. براي نيل به اين هدف، در ابتدا ابزار مدل سازي فرمال اعم از جبري و مبتني بر مدل بررسي و مقايسه شده است. سپس با تشريح تكنولوژي مجازي سازي در سيستم هاي كامپيوتري، يك ديتا سنتر نمونه كوچك مطابق استانداردهاي ديتا سنترها طراحي شده و سپس در لايه هاي مختلف توسط شبكه هاي پتري مدل گرديده است. اين مدل سازي از سطح كاملا انتزاعي (لايه 1) براي كل ديتا سنتر شروع و با طراحي مدل براي زير سيستم ها و مكانيزم هايي مانند ساختار شبكه، ذخيره سازي و نيز سرويس هاي سطح بالا مانند HA و Fault Tolerance پايان مي يابد. در پايان هر بخش، پس از ارائه و تشريح مدل، به تحليل و ارزيابي آن و بررسي خصوصيات رفتاري سيستم از روي مدل فرمال آن پرداخته شده است. در نهايت، نتيجه گيري از ميزان خوش رفتاري بخش هاي مختلف اين لايه در ديتا سنتر ارائه شده است.