Software-intensive safety critical systems are becoming more and more widespread and are involved in many aspects of our daily lives. Since a failure of these systems could lead to unacceptable consequences, it is imperative to guarantee high safety standards. In practice, as a way to handle their increasing complexity, these systems are often modelled as hierarchical systems. To date, a good deal of work has focused on the definition and analysis of hierarchical modelling languages and on their integration within model-driven development frameworks. Less work, however, has been directed towards formalisms to effectively express, in a precise and rigorous way, relevant behavioural properties of such systems (e.g.: safety requirements). In this work, we propose a novel extension of classic Linear Temporal Logic (LTL) called Hierarchical Linear Temporal Logic (HLTL), designed to express, in a natural yet rigorous way, behavioural properties of hierarhical systems. The formalism we propose does not commit to any specific modelling language, and can be used to predicate over a large variety of hierarchical systems.

Expressing Structural Temporal Properties of Safety Critical Hierarchical Systems

Peron A.;
2021-01-01

Abstract

Software-intensive safety critical systems are becoming more and more widespread and are involved in many aspects of our daily lives. Since a failure of these systems could lead to unacceptable consequences, it is imperative to guarantee high safety standards. In practice, as a way to handle their increasing complexity, these systems are often modelled as hierarchical systems. To date, a good deal of work has focused on the definition and analysis of hierarchical modelling languages and on their integration within model-driven development frameworks. Less work, however, has been directed towards formalisms to effectively express, in a precise and rigorous way, relevant behavioural properties of such systems (e.g.: safety requirements). In this work, we propose a novel extension of classic Linear Temporal Logic (LTL) called Hierarchical Linear Temporal Logic (HLTL), designed to express, in a natural yet rigorous way, behavioural properties of hierarhical systems. The formalism we propose does not commit to any specific modelling language, and can be used to predicate over a large variety of hierarchical systems.
2021
978-3-030-85346-4
https://link.springer.com/book/10.1007/978-3-030-85347-1
File in questo prodotto:
File Dimensione Formato  
HLTL___QUATIC_2021 (1).pdf

Open Access dal 26/08/2022

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Copyright Editore
Dimensione 440.31 kB
Formato Adobe PDF
440.31 kB Adobe PDF Visualizza/Apri
quality-of-information-and-communications-technology-2021.pdf

Accesso chiuso

Descrizione: cover, index,capitolo
Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 1.55 MB
Formato Adobe PDF
1.55 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/3032615
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact