Formal Verification of Device State Chart Models