Expressing and organizing real-time specification patterns via temporal logics

Formal specification models provide support for the formal verification and validation of the system behaviour. This advantage is typically paid in terms of effort and time spent in learning and using formal methods and tools. The introduction and usage of patterns have a double impact. They stand for examples on how to cover classical problems with formal methods in many different notations, so that the user can shorten the time to understand if a formal method can be used to meet his purpose and how it can be used. Furthermore, they are used for shortening the specification time, by reusing and composing different patterns to cover the specification, thus producing more understandable specifications which refer to commonly known patterns. For these reasons, both interests in and usage of patterns are growing and a higher number of proposals for patterns and pattern classification/organization has appeared in the literature. This paper reports a review of the state of the art for real-time specification patterns, so as to organize them in a unified way, while providing some new patterns which complete the unified model. The proposed organization is based on some relationships among patterns as demonstrated in the paper. During the presentation the patterns have been formalized in TILCO-X, whereas in appendix a list of patterns with formalizations in several different logics such as TILCO, LTL, CTL, GIL, QRE, MTL, TCTL and RTGIL, is provided disguised as links to the locations where such formalizations can be recovered and/or are directly reported, if found not accessible in the literature; this allows the reader to have a detailed view of all the classified patterns, including the ones already added. Furthermore, an example has been proposed to highlight the usefulness of the new identified patterns completing the unified model.