{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:37:39Z","timestamp":1769733459765,"version":"3.49.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319662657","type":"print"},{"value":"9783319662664","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66266-4_8","type":"book-chapter","created":{"date-parts":[[2017,8,15]],"date-time":"2017-08-15T22:33:31Z","timestamp":1502836411000},"page":"117-131","source":"Crossref","is-referenced-by-count":9,"title":["A Simplex Architecture for Hybrid Systems Using Barrier Certificates"],"prefix":"10.1007","author":[{"given":"Junxing","family":"Yang","sequence":"first","affiliation":[]},{"given":"Md. Ariful","family":"Islam","sequence":"additional","affiliation":[]},{"given":"Abhishek","family":"Murthy","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]},{"given":"Scott D.","family":"Stoller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,17]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-36580-X_5","volume-title":"Hybrid Systems: Computation and Control","author":"E Asarin","year":"2003","unstructured":"Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20\u201335. Springer, Heidelberg (2003). doi: 10.1007\/3-540-36580-X_5"},{"key":"8_CR2","unstructured":"Bak, S.: Verifiable COTS-Based Cyber-Physical Systems. Ph.D. thesis, University of Illinois at Urbana-Champaign (2013)"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Bak, S., Manamcheri, K., Mitra, S., Caccamo, M.: Sandboxing controllers for cyber-physical systems. In: Proceedings of the 2011 IEEE\/ACM International Conference on Cyber-Physical Systems, ICCPS, pp. 3\u201312. IEEE Computer Society (2011)","DOI":"10.1109\/ICCPS.2011.25"},{"key":"8_CR4","doi-asserted-by":"crossref","DOI":"10.1137\/1.9781611970777","volume-title":"Linear Matrix Inequalities in System and Control Theory","author":"SP Boyd","year":"1994","unstructured":"Boyd, S.P., El Ghaoui, L., Feron, E., Balakrishnan, V.: Linear Matrix Inequalities in System and Control Theory, vol. 15. SIAM, Philadelphia (1994)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: Real-Time Systems Symposium (RTSS), pp. 13\u201324. IEEE (2016)","DOI":"10.1109\/RTSS.2016.011"},{"issue":"1","key":"8_CR6","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"A Chutinan","year":"2003","unstructured":"Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64\u201375 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-64358-3_34","volume-title":"Hybrid Systems: Computation and Control","author":"T Dang","year":"1998","unstructured":"Dang, T., Maler, O.: Reachability analysis via face lifting. In: Henzinger, T.A., Sastry, S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 96\u2013109. Springer, Heidelberg (1998). doi: 10.1007\/3-540-64358-3_34"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-31954-2_20","volume-title":"Hybrid Systems: Computation and Control","author":"S Glavaski","year":"2005","unstructured":"Glavaski, S., Papachristodoulou, A., Ariyur, K.: Safety verification of controlled advanced life support system using barrier certificates. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 306\u2013321. Springer, Heidelberg (2005). doi: 10.1007\/978-3-540-31954-2_20"},{"issue":"2","key":"8_CR9","first-page":"26","volume":"15","author":"TT Johnson","year":"2016","unstructured":"Johnson, T.T., Bak, S., Caccamo, M., Sha, L.: Real-time reachability for verified simplex design. ACM Trans. Embed. Comput. Syst. (TECS) 15(2), 26 (2016)","journal-title":"ACM Trans. Embed. Comput. Syst. (TECS)"},{"key":"8_CR10","unstructured":"Loechner, V.: Polylib: A library for manipulating parameterized polyhedra (1999)"},{"key":"8_CR11","unstructured":"Murthy, A., Bartocci, E., Zadok, E., Stoller, S., Smolka, S., Grosu, R.: Simplex architecture for run time assurance of hybrid systems. In: Safe and Secure Systems and Software Symposium (S5) (2012)"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Murthy, A., Islam, M.A., Smolka, S.A., Grosu, R.: Computing bisimulation functions using SOS optimization and $$\\delta $$ -decidability over the reals. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 78\u201387. ACM, New York (2015)","DOI":"10.1145\/2728606.2728609"},{"key":"8_CR13","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/j.nahs.2016.03.008","volume":"23","author":"A Murthy","year":"2017","unstructured":"Murthy, A., Islam, M.A., Smolka, S.A., Grosu, R.: Computing compositional proofs of input-to-output stability using sos optimization and $$\\delta $$ -decidability. Nonlinear Anal. Hybrid Syst. 23, 272\u2013286 (2017)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"8_CR14","unstructured":"Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Parrilo, P.A.: SOSTOOLS: Sum of squares optimization toolbox for MATLAB (2013)"},{"key":"8_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24743-2_32"},{"issue":"8","key":"8_CR17","doi-asserted-by":"crossref","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131429 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"8_CR18","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"JD Quesel","year":"2016","unstructured":"Quesel, J.D., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with keymaera: a tutorial on safety. Int. J. Softw. Tools Technol. Transf. 18(1), 67\u201391 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Seto, D., Sha, L.: An engineering method for safety region development. Technical Report CMU\/SEI-99-TR-018, Software Engineering Institute (1999)","DOI":"10.21236\/ADA367624"},{"issue":"4","key":"8_CR20","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1109\/MS.2001.936213","volume":"18","author":"L Sha","year":"2001","unstructured":"Sha, L.: Using simplicity to control complexity. IEEE Softw. 18(4), 20\u201328 (2001)","journal-title":"IEEE Softw."},{"issue":"7","key":"8_CR21","doi-asserted-by":"crossref","first-page":"986","DOI":"10.1109\/JPROC.2003.814621","volume":"91","author":"CJ Tomlin","year":"2003","unstructured":"Tomlin, C.J., Mitchell, I., Bayen, A.M., Oishi, M.: Computational techniques for the verification of hybrid systems. Proc. IEEE 91(7), 986\u20131001 (2003)","journal-title":"Proc. IEEE"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Wang, L., Ames, A.D., Egerstedt, M.: Multi-objective compositions for collision-free connectivity maintenance in teams of mobile robots. CoRR abs\/1608.06887 (2016)","DOI":"10.1109\/CDC.2016.7798663"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66266-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T08:38:33Z","timestamp":1570005513000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66266-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319662657","9783319662664"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66266-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}