Patterns for Timed Property Specifications

Patterns for property specification enable non-experts to write formal specifications that can be used for automatic model checking. The existing patterns identified in [6] allow to reason about occurrence and order of events, but not about their timing. We extend this pattern system by patterns related to time. This allows the specification of real-time requirements. Key words: patterns, formal specification, timed model checking, verification

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Volker Gruhn, Ralf Laue
• Keywords: ENTCS 2006, Formal Specification, Property Specification, Specification