{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:26:17Z","timestamp":1725909977412},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319675305"},{"type":"electronic","value":"9783319675312"}],"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-67531-2_5","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"68-84","source":"Crossref","is-referenced-by-count":5,"title":["Combining Symbolic Runtime Enforcers for Cyber-Physical Systems"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Andersson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sagar","family":"Chaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dionisio","family":"de Niz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"5_CR1","unstructured":"NSF Definition of Cyber-Physical Systems. https:\/\/www.nsf.gov\/funding\/pgm_summ.jsp?pims_id=503286"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Bak, S., Johnson, T., Caccamo, M., Sha, L.: Real-time reachability for verified simplex design. In: Proceedings of the 35th Real-Time Systems Symposium, RTSS 2014 (2014)","DOI":"10.1109\/RTSS.2014.21"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Basin, D., Jug\u00e9, V., Klaedtke, F., Z\u0103linescu, E.: Enforceable security policies revisited. ACM Trans. Inf. Syst. Secur. (TISSEC) (2013)","DOI":"10.1145\/2487222.2487225"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$vZ$$ - An optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_14"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-46681-0_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: runtime enforcement for reactive systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533\u2013548. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_51"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"deNiz, D., Lakshmanan, K., Rajkumar, R.: On the scheduling of mixed-criticality real-time task sets. In: Proceedings of the 30th Real-Time Systems Symposium, RTSS 2009 (2009)","DOI":"10.1109\/RTSS.2009.46"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10703-011-0114-4","volume":"38","author":"Y Falcone","year":"2011","unstructured":"Falcone, Y., Mounier, L., Fernandez, J.C., Ricier, J.L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form. Methods Syst. Des. (FMSD) 38, 223\u2013262 (2011)","journal-title":"Form. Methods Syst. Des. (FMSD)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Fong, P.: Access control by tracking shallow execution history. In: IEEE Security and Privacy (2004)","DOI":"10.1109\/SECPRI.2004.1301314"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-69149-5_40","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K Havelund","year":"2008","unstructured":"Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 374\u2013383. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-69149-5_40"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Monitoring programs using rewriting. In: Proceedings of the 16th International Conference on Automated Software Engineering, ASE 2001 (2001)","DOI":"10.1109\/ASE.2001.989799"},{"key":"5_CR11","unstructured":"Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: Formally specified monitoring of temporal properties. In: Proceedings of the 11th Euromicro Conference on Real-Time Systems, ECRTS 1999 (1999)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Leucker, M., Schallhart, C.: A brief account of runtime verification. In: JLAP (2008)","DOI":"10.1007\/978-3-540-89247-2"},{"key":"5_CR13","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. (IJIS) 4, 2\u201316 (2005)","journal-title":"Int. J. Inf. Secur. (IJIS)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"5_CR15","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/s11334-013-0223-x","volume":"9","author":"L Pike","year":"2013","unstructured":"Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: monitoring embedded systems. Innov. Syst. Softw. Eng. (ISSE) 9, 235\u2013255 (2013)","journal-title":"Innov. Syst. Softw. Eng. (ISSE)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Falcone, Y., J\u00e9ron, T., Marchand, H., Rollet, A., Timo, O.: Runtime enforcement of timed properties. In: Proceedings of the 2nd International Conference on Runtime Verification, RV 2012 (2012)","DOI":"10.1007\/978-3-642-35632-2_23"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Pinisetty, S., Roop, P., Smyth, S., Tripakis, S., Hanxleden, R.: Runtime enforcement of reactive systems using synchronous enforcers. coRR abs\/1612.05030 (2016)","DOI":"10.1145\/3092282.3092291"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-40648-0_7","volume-title":"NASA Formal Methods","author":"S Pinisetty","year":"2016","unstructured":"Pinisetty, S., Tripakis, S.: Compositional runtime enforcement. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 82\u201399. Springer, Cham (2016). doi: 10.1007\/978-3-319-40648-0_7"},{"key":"5_CR19","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F Schneider","year":"2000","unstructured":"Schneider, F.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. (TISSEC) 3, 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Seto, D., Krogh, B., Sha, L., Chutinan, A.: The simplex architecture for safe online control system upgrades. In: Proceedings of the American Control Conference (1998)","DOI":"10.1109\/ACC.1998.703255"},{"key":"5_CR21","unstructured":"Viswanatha, M.: Foundations for the run-time analysis of software systems. Ph.D. thesis, University of Pennsylvania (2000)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-319-40648-0_6","volume-title":"NASA Formal Methods","author":"M Wu","year":"2016","unstructured":"Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 65\u201381. Springer, Cham (2016). doi: 10.1007\/978-3-319-40648-0_6"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T04:19:15Z","timestamp":1570076355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}