{Property Specification Patterns for Finite-State Verification}