Patterns for Timed Property Specifications

TLDR

Patterns for property specification enable non‑experts to write formal specifications for automatic model checking, but existing patterns only address event occurrence and order, not timing. The authors extend the pattern system with timing‑related patterns. The extended patterns enable specification of real‑time requirements.

Abstract

Patterns for property specification enable non-experts to write formal specifications that can be used for automatic model checking. The existing patterns identified in [Dwyer, M.B., G.S. Avrunin and J.C. Corbett, Property specification patterns for finite-state verification, in: FMSP '98: Proceedings of the second workshop on Formal methods in software practice (1998), pp. 7–15] 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.