We introduce a new logic called Signal Convolution Logic (SCL) that combines temporal logic with convolutional filters from digital signal processing. SCL enables to reason about the percentage of time a formula is satisfied in a bounded interval. We demonstrate that this new logic is a suitable formalism to effectively express non-functional requirements in Cyber-Physical Systems displaying noisy and irregular behaviours. We define both a qualitative and quantitative semantics for it, providing an efficient monitoring procedure. Finally, we prove SCL at work to monitor the artificial pancreas controllers that are employed to automate the delivery of insulin for patients with type-1 diabetes.

Signal Convolution Logic

Silvetti, Simone
Membro del Collaboration Group
;
Nenzi, Laura
Membro del Collaboration Group
;
Bortolussi, Luca
Membro del Collaboration Group
2018-01-01

Abstract

We introduce a new logic called Signal Convolution Logic (SCL) that combines temporal logic with convolutional filters from digital signal processing. SCL enables to reason about the percentage of time a formula is satisfied in a bounded interval. We demonstrate that this new logic is a suitable formalism to effectively express non-functional requirements in Cyber-Physical Systems displaying noisy and irregular behaviours. We define both a qualitative and quantitative semantics for it, providing an efficient monitoring procedure. Finally, we prove SCL at work to monitor the artificial pancreas controllers that are employed to automate the delivery of insulin for patients with type-1 diabetes.
File in questo prodotto:
File Dimensione Formato  
Silvetti et al_2018_Signal Convolution Logic.pdf

Open Access dal 01/10/2019

Descrizione: Authors may self-archive the author’s accepted manuscript of their articles on their own websites. Authors may also deposit this version of the article in any repository, provided it is only made publicly available 12 months after official publication or later. He/ she may not use the publisher's version (the final article), which is posted on SpringerLink and other Springer websites, for the purpose of self-archiving or deposit. Furthermore, the author may only post his/her version provided acknowledgement is given to the original source of publication and a link is inserted to the published article on Springer's website. The link must be provided by inserting the DOI number of the article in the following sentence: “The final publication is available at Springer via http://dx.doi.org/0.1007/978-3-030-01090-4 _ 16
Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Copyright Editore
Dimensione 1.47 MB
Formato Adobe PDF
1.47 MB Adobe PDF Visualizza/Apri
front matter+Bortolussi1.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 1.01 MB
Formato Adobe PDF
1.01 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

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/2931408
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 5
social impact