1. Alimguzhin, V., Mari, F., Melatti, I., Salvo, I., Tronci, E.: Linearising discrete time hybrid systems. IEEE Transactions on Automatic Control PP(99), 1 (2017)

   Google Scholar 

2. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993).https://doi.org/10.1007/3-540-57318-6_30

   Chapter  Google Scholar 

3. Ames, A.D., Holley, J.: Quadratic program based nonlinear embedded control of series elastic actuators. In CDC, pp. 6291–6298. IEEE (2014)

   Google Scholar 

4. 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)

   Article MATH MathSciNet  Google Scholar 

5. Bortolussi, L., Milios, D., Sanguinetti, G.: U-Check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89–104. Springer, Cham (2015).https://doi.org/10.1007/978-3-319-22264-6_6

   Chapter  Google Scholar 

6. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58–75. Springer, Heidelberg (2017).https://doi.org/10.1007/978-3-662-54577-5_4

   Chapter  Google Scholar 

7. David, A., Larsen, K., Legay, A., Mikučionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. International Journal on Software Tools for Technology Transfer17(4), 397–415 (2015)

   Article  Google Scholar 

8. de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).https://doi.org/10.1007/978-3-540-78800-3_24

   Chapter  Google Scholar 

9. Duong, P.L.T., Lee, M.: Robust PID controller design for processes with stochastic parametric uncertainties. Journal of Process Control22(9), 1559–1566 (2012)

   Article  Google Scholar 

10. Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008).https://doi.org/10.1007/978-3-540-88387-6_14

    Chapter  Google Scholar 

11. Ellen, C., Gerwinn, S., Fränzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. International Journal on Software Tools for Technology Transfer17(4), 485–504 (2015)

    Article  Google Scholar 

12. Farahani, S.S., Raman, V., Murray, R.M.: Robust model predictive control for signal temporal logic synthesis. In: ADHS (2015)

    Google Scholar 

13. Fliess, M., Join, C.: Model-free control. International Journal of Control86(12), 2228–2252 (2013)

    Article MATH MathSciNet  Google Scholar 

14. Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: HSCC, pp. 43–52 (2011)

    Google Scholar 

15. Fränzle, M., Teige, T., Eggers, A.: Engineering constraint solvers for automatic analysis of probabilistic hybrid automata. J. Log. Algebr. Program.79(7), 436–466 (2010)

    Article MATH MathSciNet  Google Scholar 

16. Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS, pp. 305–314 (2012)

    Google Scholar 

17. Gao, S., Kong, S., Clarke, E.M.:dReal: An SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013).https://doi.org/10.1007/978-3-642-38574-2_14

    Chapter  Google Scholar 

18. Guo, L., Wang, H.: PID controller design for output PDFs of stochastic systems using linear matrix inequalities. IEEE T. Sys, Man, and Cyb., Part B (Cyb.)35(1), 65–71 (2005)

    Google Scholar 

19. He, S., Liu, F.: Robust stabilization of stochastic markovian jumping systems via proportional-integral control. Signal Processing91(11), 2478–2486 (2011)

    Article MATH  Google Scholar 

20. Hovorka, R.: Closed-loop insulin delivery: from bench to clinical practice. Nature Reviews Endocrinology7(7), 385–395 (2011)

    Google Scholar 

21. Hovorka, R., et al.: Nonlinear model predictive control of glucose concentration in subjects with type 1 diabetes. Physiological Measurement25(4), 905 (2004)

    Google Scholar 

22. Huyett, L.M., et al.: Design and evaluation of a robust PID controller for a fully implantable artificial pancreas. Industrial & Engineering Chemistry Research54(42), 10311–10321 (2015)

    Article  Google Scholar 

23. Kanderian Jr., S.S., Steil, G.M.: Apparatus and method for controlling insulin infusion with state variable feedback, July 15 (2014). US Patent 8,777,924

    Google Scholar 

24. Levine, W.S.: The control handbook. CRC Press (1996)

    Google Scholar 

25. Li, Y., Ang, K.H., Chong, G.C., Feng, W., Tan, K.C., Kashiwagi, H.: CAutoCSD-evolutionary search and optimisation enabled computer automated control system design. International Journal of Automation and Computing1(1), 76–88 (2004)

    Article  Google Scholar 

26. Mancini, T., Mari, F., Massini, A., Melatti, I., Merli, F., Tronci, E.: System level formal verification via model checking driven simulation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 296–312. Springer, Heidelberg (2013).https://doi.org/10.1007/978-3-642-39799-8_21

    Chapter  Google Scholar 

27. Paoletti, N., Liu, K.S., Smolka, S.A., Lin, S.: Data-driven robust control for type 1 diabetes under meal and exercise uncertainties. In: Feret, J., Koeppl, H. (eds.) CMSB 2017. LNCS, vol. 10545, pp. 214–232. Springer, Cham (2017).https://doi.org/10.1007/978-3-319-67471-1_13

    Chapter  Google Scholar 

28. Parker, R.S., Doyle, F.J., Ward, J.H., Peppas, N.A.: Robust H\(_\infty \) glucose control in diabetes using a physiological model. AIChE Journal46(12), 2537–2549 (2000)

    Article  Google Scholar 

29. Sha, L.: Using simplicity to control complexity. IEEE Software18(4), 20–28 (2001)

    Article  Google Scholar 

30. Shmarov, F., Paoletti, N., Bartocci, E., Lin, S., Smolka, S.A., Zuliani, P.: Automated synthesis of safe and robust PID controllers for stochastic hybrid systems (2017).arxiv:1707.05229

31. Shmarov, F., Zuliani, P.: ProbReach: Verified probabilistic\(\delta \)-reachability for stochastic hybrid systems. In HSCC, pp. 134–139. ACM (2015)

    Google Scholar 

32. Shmarov, F., Zuliani, P.: Probabilistic hybrid systems verification via SMT and Monte Carlo techniques. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 152–168. Springer, Cham (2016).https://doi.org/10.1007/978-3-319-49052-6_10

    Chapter  Google Scholar 

33. Steil, G.M., et al.: The effect of insulin feedback on closed loop glucose control. The Journal of Clinical Endocrinology & Metabolism96(5), 1402–1408 (2011)

    Article  Google Scholar 

34. Su, Y., Sun, D., Duan, B.: Design of an enhanced nonlinear PID controller. Mechatronics15(8), 1005–1024 (2005)

    Article  Google Scholar 

35. Szalay, P., Eigner, G., Kovács, L.A.: Linear matrix inequality-based robust controller design for type-1 diabetes model. IFAC Proceedings Volumes47(3), 9247–9252 (2014)

    Article  Google Scholar 

36. Wilinska, M.E., et al.: Simulation environment to evaluate closed-loop insulin delivery systems in type 1 diabetes. Journal of diabetes science and technology4(1), 132–144 (2010)

    Article  Google Scholar 

37. Zhang, L., She, Z., Ratschan, S., Hermanns, H., Hahn, E.M.: Safety verification for probabilistic hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 196–211. Springer, Heidelberg (2010).https://doi.org/10.1007/978-3-642-14295-6_21

    Chapter  Google Scholar 

Download references