Modeling and Formal Verification of Smart Environments