Smart Building Management Systems is rapidly growing worldwide mainly to reduceenergy consumption and carbon footprints. Some other benefits that can be achievedthrough this system include lowering operational costs and increasing occupant’s comfort,safety, and increased productivity. Programmable Logic Controllers (PLCs) areused widely for automating smart buildings. The vulnerabilities and attack surfacesof PLCs enable an attacker to control the smart building in order to cause more energyusage, target specific people, and destroy assets. This thesis summarizes the vulnerabilities,threats, and attacks for PLC-based systems. Moreover, the current stateof the art of static and dynamic analysis, threat and attack detection, automation,and conflict analysis of smart buildings are discussed. This thesis aims at detecting,analyzing, and mitigating the attack surfaces that are possible for smart buildings.A formal methods approach is proposed for detecting safety and security propertyviolations for smart buildings. Then, a rule-based method is developed to detect violationsleveraging provenance data collected from the system. These safety violatingincidences are mapped to corresponding variables in a PLC source program. Finally,we implement defeasible reasoning that enforces safety properties in the system. Weverify that not only does the new PLC program adhere to the safety properties thathave been instrumented, but also it does not trigger any new safety property violations.Finally, we outline new directions to be investigated in the future.