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, LauraMembro del Collaboration Group
;Bortolussi, LucaMembro 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 | 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.
