{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T03:53:55Z","timestamp":1769918035465,"version":"3.49.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319489889","type":"print"},{"value":"9783319489896","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_10","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T06:31:19Z","timestamp":1478500279000},"page":"155-163","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation"],"prefix":"10.1007","author":[{"given":"Yuqi","family":"Chen","sequence":"first","affiliation":[]},{"given":"Christopher M.","family":"Poskitt","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"10_CR1","unstructured":"Secure Water Treatment (SWaT). http:\/\/itrust.sutd.edu.sg\/research\/testbeds\/secure-water-treatment-swat\/ . Accessed Sep 2016"},{"key":"10_CR2","unstructured":"Supplementary material. http:\/\/sav.sutd.edu.sg\/?page_id=3258"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Adepu, S., Mathur, A.: Distributed detection of single-stage multipoint cyber attacks in a water treatment plant. In: Proceedings of ACM Asia Conference on Computer and Communications Security (AsiaCCS 2016), pp. 449\u2013460. ACM (2016)","DOI":"10.1145\/2897845.2897855"},{"key":"10_CR4","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-319-33630-5_7","volume-title":"Proceedings of International Conference on ICT Systems Security and Privacy Protection (SEC 2016)","author":"S Adepu","year":"2016","unstructured":"Adepu, S., Mathur, A.: Using process invariants to detect cyber attacks on a water treatment system. In: Hoepman, J.-H., Katzenbeisser, S. (eds.) Proceedings of International Conference on ICT Systems Security and Privacy Protection (SEC 2016). IFIP AICT, vol. 471, pp. 91\u2013104. Springer, New York (2016)"},{"key":"10_CR5","unstructured":"Alves, T., Felton, D.: TrustZone: integrated hardware and software security. ARM white paper (2004)"},{"key":"10_CR6","unstructured":"Anati, I., Gueron, S., Johnson, S.P., Scarlata, V.R.: Innovative technology for CPU based attestation and sealing. Intel white paper (2013)"},{"key":"10_CR7","unstructured":"C\u00e1rdenas, A.A., Amin, S., Sastry, S.: Research challenges for the security of control systems. In: Proceedings of USENIX Workshop on Hot Topics in Security (HotSec 2008). USENIX Association (2008)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Castelluccia, C., Francillon, A., Perito, D., Soriente, C.: On the difficulty of software-based attestation of embedded devices. In: Proceedings of ACM Conference on Computer and Communications Security (CCS 2009), pp. 400\u2013409. ACM (2009)","DOI":"10.1145\/1653662.1653711"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Choudhari, A., Ramaprasad, H., Paul, T., Kimball, J.W., Zawodniok, M.J., McMillin, B.M., Chellappan, S.: Stability of a cyber-physical smart grid system using cooperating invariants. In: Proceedings of IEEE Computer Software and Applications Conference (COMPSAC 2013), pp. 760\u2013769. IEEE (2013)","DOI":"10.1109\/COMPSAC.2013.126"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-24372-1_1","volume-title":"Automated Technology for Verification and Analysis","author":"EM Clarke","year":"2011","unstructured":"Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1\u201312. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24372-1_1"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22110-1_30"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"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\u2013214. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38574-2_14"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-31424-7_34","volume-title":"Computer Aided Verification","author":"I Hasuo","year":"2012","unstructured":"Hasuo, I., Suenaga, K.: Exercises in nonstandard static analysis of hybrid systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 462\u2013478. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_34"},{"issue":"5","key":"10_CR14","doi-asserted-by":"publisher","first-page":"649","DOI":"10.1109\/TSE.2010.62","volume":"37","author":"Y Jia","year":"2011","unstructured":"Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649\u2013678 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Kang, E., Adepu, S., Jackson, D., Mathur, A.P.: Model-based security analysis of a water treatment system. In: Proceedings of International Workshop on Software Engineering for Smart Cyber-Physical Systems (SEsCPS 2016), pp. 22\u201328. ACM (2016)","DOI":"10.1145\/2897035.2897041"},{"issue":"2","key":"10_CR16","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/JSYST.2014.2322503","volume":"9","author":"SK Khaitan","year":"2015","unstructured":"Khaitan, S.K., McCalley, J.D.: Design techniques and applications of cyberphysical systems: a survey. IEEE Syst. J. 9(2), 350\u2013365 (2015)","journal-title":"IEEE Syst. J."},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-319-48989-6_28","volume-title":"FM 2016","author":"P Kong","year":"2016","unstructured":"Kong, P., Li, Y., Chen, X., Sun, J., Sun, M., Wang, J.: Towards concolic testing for hybrid systems. In: Fitzgerald, J., et al. (eds.) FM 2016. LNCS-FM, vol. 9995, pp. 460\u2013478. Springer, Heidelberg (2016)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: Cyber physical systems: design challenges. In: Proceedings of International Symposium on Object-Oriented Real-Time Distributed Computing (ISORC 2008), pp. 363\u2013369. IEEE (2008)","DOI":"10.1109\/ISORC.2008.25"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Maier, A.: Online passive learning of timed automata for cyber-physical production systems. In: Proceedings of IEEE International Conference on Industrial Informatics (INDIN 2014), pp. 60\u201366. IEEE (2014)","DOI":"10.1109\/INDIN.2014.6945484"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-11164-3_17","volume-title":"Runtime Verification","author":"S Mitsch","year":"2014","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 199\u2013214. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-11164-3_17"},{"issue":"2","key":"10_CR21","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1145\/227607.227610","volume":"5","author":"AJ Offutt","year":"1996","unstructured":"Offutt, A.J., Lee, A., Rothermel, G., Untch, R.H., Zapf, C.: An experimental determination of sufficient mutant operators. ACM Trans. Softw. Eng. Methodol. (TOSEM) 5(2), 99\u2013118 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol. (TOSEM)"},{"issue":"1","key":"10_CR22","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1109\/TSG.2013.2283171","volume":"5","author":"T Paul","year":"2014","unstructured":"Paul, T., Kimball, J.W., Zawodniok, M.J., Roth, T.P., McMillin, B.M., Chellappan, S.: Unified invariants for cyber-physical switched system stability. IEEE Trans. Smart Grid 5(1), 112\u2013120 (2014)","journal-title":"IEEE Trans. Smart Grid"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_15"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"J Quesel","year":"2016","unstructured":"Quesel, J., Mitsch, S., Loos, S.M., Arechiga, 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":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-03964-0_9","volume-title":"Critical Information Infrastructures Security","author":"T Roth","year":"2013","unstructured":"Roth, T., McMillin, B.: Physical attestation of cyber processes in the smart grid. In: Luiijf, E., Hartel, P. (eds.) CRITIS 2013. LNCS, vol. 8328, pp. 96\u2013107. Springer, Heidelberg (2013). doi: 10.1007\/978-3-319-03964-0_9"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Seshadri, A., Perrig, A., van Doorn, L., Khosla, P.K.: SWATT: software-based ATTestation for embedded devices. In: Proceedings of IEEE Symposium on Security and Privacy (S&P 2004), p. 272. IEEE (2004)","DOI":"10.1109\/SECPRI.2004.1301329"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Valente, J., Barreto, C., C\u00e1rdenas, A.A.: Cyber-physical systems attestation. In: Proceedings of IEEE International Conference on Distributed Computing in Sensor Systems (DCOSS 2014), pp. 354\u2013357. IEEE (2014)","DOI":"10.1109\/DCOSS.2014.61"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Vodencarevic, A., Kleine B\u00fcning, H., Niggemann, O., Maier, A.: Identifying behavior models for process plants. In: Proceedings of IEEE Conference on Emerging Technologies & Factory Automation (ETFA 2011), pp. 1\u20138. IEEE (2011)","DOI":"10.1109\/ETFA.2011.6059080"},{"key":"10_CR29","unstructured":"Wang, J., Sun, J., Yuan, Q., Pang, J.: Should we learn probabilistic models for model checking? a new approach and an empirical study. CoRR abs\/1605.08278 (2016). http:\/\/arxiv.org\/abs\/1605.08278"},{"issue":"99","key":"10_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/JSYST.2015.2496293","volume":"PP","author":"X Zheng","year":"2015","unstructured":"Zheng, X., Julien, C., Kim, M., Khurshid, S.: Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Syst. J. PP(99), 1\u201314 (2015)","journal-title":"IEEE Syst. J."}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T01:26:54Z","timestamp":1749691614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fm2016.cs.ucy.ac.cy\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}