Expressing and Organizing Real Time Specification Patterns via Temporal Logics

Metadata

Lingua dei metadati

Titolo Expressing and Organizing Real Time Specification Patterns via Temporal Logics

Soggetto Temporal Logic, temporal reasoning, real time temporal logic, metric of time, executable temporal logic, verification and validation, state machines

Descrizione Temporal Logic, temporal reasoning, real time temporal logic, metric of time, executable temporal logic, verification and validation, state machines

Descrizione 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/ organisation has appeared in literature. This paper reports a review of the state of the art for real-time specification patterns, so as to organise 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 formalised 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, 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 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.

Descrizione P. Bellini, P. Nesi, D. Rogai, “Expressing and organizing real-time specification patterns via temporal logics”, Journal of Systems and Software, Elsevier, Vol.82, N.2, Feb. 2009, pages 183-196, http://www.sciencedirect.com/science/article/B6V0N-4SXYFVY-3/2/0ccbc07dad5a328a8891836b2deff91e

Tecnico

Classificazione

IPR: informazioni

Luogo

Azioni

New Menu

Related objects by text

Commenti

collection's Playback

Metadata

Azioni

Filtri di Ricerca

Contenuti

Organizza collezioni personali

Classificazione