Advertisement

Signal Convolution Logic

  • Simone SilvettiEmail author
  • Laura Nenzi
  • Ezio Bartocci
  • Luca Bortolussi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

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.

References

  1. 1.
    Akazaki, Takumi, Hasuo, Ichiro: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, Daniel, Păsăreanu, Corina S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356–374. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_21CrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)MathSciNetCrossRefGoogle Scholar
  4. 4.
    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_5CrossRefGoogle Scholar
  5. 5.
    Cameron, Fraser, Fainekos, Georgios, Maahs, David M., Sankaranarayanan, Sriram: Towards a verified artificial pancreas: challenges and solutions for runtime verification. In: Bartocci, Ezio, Majumdar, Rupak (eds.) RV 2015. LNCS, vol. 9333, pp. 3–17. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-23820-3_1CrossRefGoogle Scholar
  6. 6.
    Donzé, Alexandre: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, Tayssir, Cook, Byron, Jackson, Paul (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14295-6_17CrossRefGoogle Scholar
  7. 7.
    Donzé, Alexandre, Maler, Oded: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, Krishnendu, Henzinger, Thomas A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15297-9_9CrossRefzbMATHGoogle Scholar
  8. 8.
    Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using S-TaLiRo. In: Proceedings of ACC. IEEE (2012)Google Scholar
  9. 9.
    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)MathSciNetCrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)MathSciNetCrossRefGoogle Scholar
  12. 12.
    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)Google Scholar
  13. 13.
    Maler, Oded, Nickovic, Dejan: Monitoring temporal properties of continuous signals. In: Lakhnech, Yassine, Yovine, Sergio (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30206-3_12CrossRefzbMATHGoogle Scholar
  14. 14.
    Rodionova, A., Bartocci, E., Ničković, D., Grosu, R.: Temporal logic as filtering. In: Proceedings of HSCC 2016, pp. 11–20. ACM (2016)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proc. of HSCC. pp. 125–134 (2012)Google Scholar
  17. 17.
    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). MarCrossRefGoogle Scholar
  18. 18.
    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)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Simone Silvetti
    • 1
    • 2
    Email author
  • Laura Nenzi
    • 3
  • Ezio Bartocci
    • 3
  • Luca Bortolussi
    • 4
  1. 1.DIMA, University of UdineUdineItaly
  2. 2.Esteco S.p.A.TriesteItaly
  3. 3.TU WienViennaAustria
  4. 4.DMG, University of TriesteTriesteItaly

Personalised recommendations