Skip to main content
Top

2018 | OriginalPaper | Chapter

Signal Convolution Logic

Authors : Simone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We introduce a new logic called Signal Convolution Logic (\(\text {SCL}\)) that combines temporal logic with convolutional filters from digital signal processing. \(\text {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 \(\text {SCL}\) at work to monitor the artificial pancreas controllers that are employed to automate the delivery of insulin for patients with type-1 diabetes.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
This operation is in fact a cross-correlation, but here we use the same convention of the deep learning community and call it convolution.
 
2
\(\mathcal {N}(\mu ,\sigma ^2)\) is the Gaussian distribution with mean \(\mu \) and variance \(\sigma ^2\).
 
Literature
2.
go back to reference Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB, pp. 164–177. Springer, Berlin (2013)CrossRef Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Proceedings of CMSB, pp. 164–177. Springer, Berlin (2013)CrossRef
3.
go back to reference Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3–25 (2015)MathSciNetCrossRef Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: System design of stochastic models using robustness of temporal properties. Theor. Comput. Sci. 587, 3–25 (2015)MathSciNetCrossRef
4.
go back to reference Bartocci, Ezio, Deshmukh, Jyotirmoy, Donzé, Alexandre, Fainekos, Georgios, Maler, Oded, Ničković, Dejan, Sankaranarayanan, Sriram: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, Ezio, Falcone, Yliès (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_5CrossRef Bartocci, Ezio, Deshmukh, Jyotirmoy, Donzé, Alexandre, Fainekos, Georgios, Maler, Oded, Ničković, Dejan, Sankaranarayanan, Sriram: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, Ezio, Falcone, Yliès (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018). https://​doi.​org/​10.​1007/​978-3-319-75632-5_​5CrossRef
5.
8.
go back to reference Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: Proceedings of ACC. IEEE (2012) Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: Proceedings of ACC. IEEE (2012)
9.
go back to reference Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRef Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRef
10.
go back to reference Hovorka, R., Canonico, V., Chassin, L.J., Haueter, U., Massi-Benedetti, M., Federici, M.O., Pieber, T.R., Schaller, H.C., Schaupp, L., Vering, T.: Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiol. Meas. 25(4), 905 (2004)CrossRef Hovorka, R., Canonico, V., Chassin, L.J., Haueter, U., Massi-Benedetti, M., Federici, M.O., Pieber, T.R., Schaller, H.C., Schaupp, L., Vering, T.: Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiol. Meas. 25(4), 905 (2004)CrossRef
11.
go back to reference Jha, S., Raman, V., Sadigh, D., Seshia, S.A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic. J. Autom. Reason. 60(1), 43–62 (2018)MathSciNetCrossRef Jha, S., Raman, V., Sadigh, D., Seshia, S.A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic. J. Autom. Reason. 60(1), 43–62 (2018)MathSciNetCrossRef
12.
go back to reference Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of MEMOCODE, pp. 5–14. ACM (2017) Li, J., Nuzzo, P., Sangiovanni-Vincentelli, A., Xi, Y., Li, D.: Stochastic contracts for cyber-physical system design under probabilistic requirements. In: Proceedings of MEMOCODE, pp. 5–14. ACM (2017)
14.
go back to reference Rodionova, A., Bartocci, E., Ničković, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016, pp. 11–20. ACM (2016) Rodionova, A., Bartocci, E., Ničković, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016, pp. 11–20. ACM (2016)
15.
go back to reference Sadigh, D., Kapoor, A.: Safe control under uncertainty with probabilistic signal temporal logic. In: Robotics: Science and Systems XII, University of Michigan, Ann Arbor, Michigan, USA, June 18 - June 22, 2016 (2016) Sadigh, D., Kapoor, A.: Safe control under uncertainty with probabilistic signal temporal logic. In: Robotics: Science and Systems XII, University of Michigan, Ann Arbor, Michigan, USA, June 18 - June 22, 2016 (2016)
16.
go back to reference Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proc. of HSCC. pp. 125–134 (2012) Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proc. of HSCC. pp. 125–134 (2012)
17.
go back to reference Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24–33 (2017). MarCrossRef Sankaranarayanan, S., Kumar, S.A., Cameron, F., Bequette, B.W., Fainekos, G., Maahs, D.M.: Model-based falsification of an artificial pancreas control system. SIGBED Rev. 14(2), 24–33 (2017). MarCrossRef
18.
go back to reference Shmarov, F., Paoletti, N., Bartocci, E., Lin, S., Smolka, S.A., Zuliani, P.: SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems. In: Proceedings of HVC, pp. 131–146 (2017)CrossRef Shmarov, F., Paoletti, N., Bartocci, E., Lin, S., Smolka, S.A., Zuliani, P.: SMT-based synthesis of safe and robust PID controllers for stochastic hybrid systems. In: Proceedings of HVC, pp. 131–146 (2017)CrossRef
Metadata
Title
Signal Convolution Logic
Authors
Simone Silvetti
Laura Nenzi
Ezio Bartocci
Luca Bortolussi
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_16

Premium Partner