{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:16Z","timestamp":1750220656940,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,30]],"date-time":"2020-11-30T00:00:00Z","timestamp":1606694400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P28187-N31"],"award-info":[{"award-number":["P28187-N31"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,11,30]]},"DOI":"10.1145\/3428757.3429146","type":"proceedings-article","created":{"date-parts":[[2021,1,27]],"date-time":"2021-01-27T11:29:07Z","timestamp":1611746947000},"page":"367-371","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards CPS Verification Engineering"],"prefix":"10.1145","author":[{"given":"Andreas","family":"M\u00fcller","sequence":"first","affiliation":[{"name":"University of Applied Sciences, Upper Austria, Hagenberg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[{"name":"Computer Science Department, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Werner","family":"Retschitzegger","sequence":"additional","affiliation":[{"name":"Department of Cooperative Information Systems, Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wieland","family":"Schwinger","sequence":"additional","affiliation":[{"name":"Department of Cooperative Information Systems, Johannes Kepler University, Linz, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,27]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178131"},{"volume-title":"Haifa Verification Conf. (LNCS), Eran Yahav (Ed.). Springer, 116--131","author":"Sergiy","key":"e_1_3_2_1_2_1","unstructured":"Sergiy Bogomolov et al. 2014. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. In Hardware and Software: Verification and Testing - 10th Int . Haifa Verification Conf. (LNCS), Eran Yahav (Ed.). Springer, 116--131 . Sergiy Bogomolov et al. 2014. Assume-Guarantee Abstraction Refinement Meets Hybrid Systems. In Hardware and Software: Verification and Testing - 10th Int. Haifa Verification Conf. (LNCS), Eran Yahav (Ed.). Springer, 116--131."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Brandon Bohrer et al. 2018. CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation. In 6th IFAC Conf. on Analysis and Design of Hybrid Systems (IFAC-PapersOnLine) Alessandro Abate et al. (Eds.). Elsevier 55--60.  Brandon Bohrer et al. 2018. CoasterX: A Case Study in Component-Driven Hybrid Systems Proof Automation. In 6th IFAC Conf. on Analysis and Design of Hybrid Systems (IFAC-PapersOnLine) Alessandro Abate et al. (Eds.). Elsevier 55--60.","DOI":"10.1016\/j.ifacol.2018.08.010"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.67210"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180231"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_17"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377659"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765890"},{"volume-title":"Proc. of the 26th Int. Workshop on Principles of Diagnosis. CEUR-WS.org, 201--208","author":"Matthew","key":"e_1_3_2_1_10_1","unstructured":"Matthew J. Daigle et al. 2015. A Structural Model Decomposition Framework for Hybrid Systems Diagnosis . In Proc. of the 26th Int. Workshop on Principles of Diagnosis. CEUR-WS.org, 201--208 . Matthew J. Daigle et al. 2015. A Structural Model Decomposition Framework for Hybrid Systems Diagnosis. In Proc. of the 26th Int. Workshop on Principles of Diagnosis. CEUR-WS.org, 201--208."},{"key":"e_1_3_2_1_11_1","volume-title":"Daigle et al","author":"Matthew","year":"2018","unstructured":"Matthew J. Daigle et al . 2018 . Diagnosis of Hybrid Systems Using Structural Model Decomposition. In Fault Diagnosis of Hybrid Dynamic and Complex Systems, Moamar Sayed-Mouchaweh (Ed.). Springer , Cham, 179--207. Matthew J. Daigle et al. 2018. Diagnosis of Hybrid Systems Using Structural Model Decomposition. In Fault Diagnosis of Hybrid Dynamic and Complex Systems, Moamar Sayed-Mouchaweh (Ed.). Springer, Cham, 179--207."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032332"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1768283.1768290"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.85"},{"key":"e_1_3_2_1_15_1","volume-title":"IEEE Conf. on Decision and Control, CDC","volume":"1","author":"Goran","unstructured":"Goran Frehse et al. 2004. Assume-guarantee reasoning for hybrid I\/O-automata by over-approximation of continuous interaction . In IEEE Conf. on Decision and Control, CDC , Vol. 1 . Goran Frehse et al. 2004. Assume-guarantee reasoning for hybrid I\/O-automata by over-approximation of continuous interaction. In IEEE Conf. on Decision and Control, CDC, Vol. 1."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032335"},{"volume-title":"Ke Ymaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. In Conf. on Automated Deduction, Proc. (LNCS). Springer.","author":"Nathan","key":"e_1_3_2_1_17_1","unstructured":"Nathan Fulton et al. 2015 . Ke Ymaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. In Conf. on Automated Deduction, Proc. (LNCS). Springer. Nathan Fulton et al. 2015. Ke Ymaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. In Conf. on Automated Deduction, Proc. (LNCS). Springer."},{"volume-title":"Proc. (LNCS). Springer.","author":"Martin","key":"e_1_3_2_1_18_1","unstructured":"Martin Hentschel et al. 2014. Symbolic Execution Debugger (SED). In Runtime Verification , Proc. (LNCS). Springer. Martin Hentschel et al. 2014. Symbolic Execution Debugger (SED). In Runtime Verification, Proc. (LNCS). Springer."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646881.710633"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377657"},{"volume-title":"2006 IEEE Power Engineering Society General Meeting.","author":"Zhenyu","key":"e_1_3_2_1_21_1","unstructured":"Zhenyu Huang et al. 2006. Model validation with hybrid dynamic simulation . In 2006 IEEE Power Engineering Society General Meeting. Zhenyu Huang et al. 2006. Model validation with hybrid dynamic simulation. In 2006 IEEE Power Engineering Society General Meeting."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461337"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/SERE-C.2012.49"},{"volume-title":"IEEE Conf. on Softw. Quality, Reliability and Security Companion. IEEE.","author":"Eun-Young","key":"e_1_3_2_1_25_1","unstructured":"Eun-Young Kang et al. 2017. Verification and Validation of a Cyber-Physical System in the Automotive Domain . In IEEE Conf. on Softw. Quality, Reliability and Security Companion. IEEE. Eun-Young Kang et al. 2017. Verification and Validation of a Cyber-Physical System in the Automotive Domain. In IEEE Conf. on Softw. Quality, Reliability and Security Companion. IEEE."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/WICSA-ECSA.212.26"},{"volume-title":"IEEE Conf. on Decision and Control. IEEE.","author":"Nikolaos","key":"e_1_3_2_1_27_1","unstructured":"Nikolaos Kekatos et al. 2017. Constructing verification models of nonlinear Simulink systems via syntactic hybridization . In IEEE Conf. on Decision and Control. IEEE. Nikolaos Kekatos et al. 2017. Constructing verification models of nonlinear Simulink systems via syntactic hybridization. In IEEE Conf. on Decision and Control. IEEE."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737166.2737180"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10796-016-9685-3"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_31_1","volume-title":"SURE: A Modeling and Simulation Integration Platform for Evaluation of Secure and Resilient Cyber-Physical Systems. IEEE Proc. 106","author":"Xenofon","year":"2018","unstructured":"Xenofon D. Koutsoukos et al. 2018 . SURE: A Modeling and Simulation Integration Platform for Evaluation of Secure and Resilient Cyber-Physical Systems. IEEE Proc. 106 , 1 ( 2018 ). Xenofon D. Koutsoukos et al. 2018. SURE: A Modeling and Simulation Integration Platform for Evaluation of Secure and Resilient Cyber-Physical Systems. IEEE Proc. 106, 1 (2018)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/570907.570930"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021304"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_33"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2134"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646880.710462"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Andre Metelo et al. 2018. Towards the Modular Specification and Validation of Cyber-Physical Systems: A Case-Study on Reservoir Modeling with Hybrid Automata. In Computational Science and Its Applications (LNCS). Springer.  Andre Metelo et al. 2018. Towards the Modular Specification and Validation of Cyber-Physical Systems: A Case-Study on Reservoir Modeling with Hybrid Automata. In Computational Science and Its Applications (LNCS). Springer.","DOI":"10.1007\/978-3-319-95162-1_6"},{"key":"e_1_3_2_1_39_1","volume-title":"Reusability Metrics of Software Components: Survey. In Centrl. Europ. Conf. on Inform. and Intell. Sys","author":"Mija\u010d Marko","year":"2015","unstructured":"Marko Mija\u010d and Zlatko Stapic . 2015 . Reusability Metrics of Software Components: Survey. In Centrl. Europ. Conf. on Inform. and Intell. Sys . Univ. Zagreb. Marko Mija\u010d and Zlatko Stapic. 2015. Reusability Metrics of Software Components: Survey. In Centrl. Europ. Conf. on Inform. and Intell. Sys. Univ. Zagreb."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2015.128"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_28"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/3288063.3288082"},{"volume-title":"Cyber Physical Systems. Model-Based Design - 8th International Workshop. Revised Selected Papers (Lecture Notes in Computer Science)","author":"M\u00fcller Andreas","key":"e_1_3_2_1_43_1","unstructured":"Andreas M\u00fcller , Stefan Mitsch , Wieland Schwinger , and Andr\u00e9 Platzer . 2018. A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration) . In Cyber Physical Systems. Model-Based Design - 8th International Workshop. Revised Selected Papers (Lecture Notes in Computer Science) , Vol. 11615 . Springer , 91--110. Andreas M\u00fcller, Stefan Mitsch, Wieland Schwinger, and Andr\u00e9 Platzer. 2018. A Component-Based Hybrid Systems Verification and Implementation Tool in KeYmaera X (Tool Demonstration). In Cyber Physical Systems. Model-Based Design - 8th International Workshop. Revised Selected Papers (Lecture Notes in Computer Science), Vol. 11615. Springer, 91--110."},{"volume-title":"Conf. (LNCS), Rajeev Alur and Insup Lee (Eds.). Springer.","author":"Sandeep","key":"e_1_3_2_1_44_1","unstructured":"Sandeep Neema et al. 2003. Constraint-Based Design-Space Exploration and Model Synthesis. In Embedded Software , Conf. (LNCS), Rajeev Alur and Insup Lee (Eds.). Springer. Sandeep Neema et al. 2003. Constraint-Based Design-Space Exploration and Model Synthesis. In Embedded Software, Conf. (LNCS), Rajeev Alur and Insup Lee (Eds.). Springer."},{"volume-title":"Automation & Test in Europe Conf. & Exhib. IEEE.","author":"Pierluigi","key":"e_1_3_2_1_45_1","unstructured":"Pierluigi Nuzzo et al. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In Design , Automation & Test in Europe Conf. & Exhib. IEEE. Pierluigi Nuzzo et al. 2018. CHASE: Contract-based requirement engineering for cyber-physical system design. In Design, Automation & Test in Europe Conf. & Exhib. IEEE."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00602-9_20"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_13"},{"key":"e_1_3_2_1_48_1","volume-title":"A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. Logical Methods in Computer Science 8, 4","author":"Platzer Andr\u00e9","year":"2012","unstructured":"Andr\u00e9 Platzer . 2012. A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. Logical Methods in Computer Science 8, 4 ( 2012 ). Andr\u00e9 Platzer. 2012. A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. Logical Methods in Computer Science 8, 4 (2012)."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/3281334"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070525"},{"key":"e_1_3_2_1_51_1","volume-title":"Specification: The Biggest Bottleneck in Formal Methods and Autonomy. In Verified Software. Theories, Tools, and Experiments Conf. (LNCS).","author":"Rozier Kristin Yvonne","year":"2016","unstructured":"Kristin Yvonne Rozier . 2016 . Specification: The Biggest Bottleneck in Formal Methods and Autonomy. In Verified Software. Theories, Tools, and Experiments Conf. (LNCS). Kristin Yvonne Rozier. 2016. Specification: The Biggest Bottleneck in Formal Methods and Autonomy. In Verified Software. Theories, Tools, and Experiments Conf. (LNCS)."},{"volume-title":"Software engineering (9. ed.)","author":"Sommerville Ian","key":"e_1_3_2_1_52_1","unstructured":"Ian Sommerville . 2011. Software engineering (9. ed.) . Pearson , Boston, MA . Ian Sommerville. 2011. Software engineering (9. ed.). Pearson, Boston, MA."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2015.04.081"},{"key":"e_1_3_2_1_54_1","volume-title":"IFAC Proc. Volumes 36","author":"Olaf","year":"2003","unstructured":"Olaf Stursberg et al. 2003. Specification-Guided Analysis of Hybrid Systems Using a Hierarchy of Validation Methods . IFAC Proc. Volumes 36 , 6 ( 2003 ), 289--294. Olaf Stursberg et al. 2003. Specification-Guided Analysis of Hybrid Systems Using a Hierarchy of Validation Methods. IFAC Proc. Volumes 36, 6 (2003), 289--294."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2015.09.019"}],"event":{"name":"iiWAS '20: The 22nd International Conference on Information Integration and Web-based Applications & Services","sponsor":["Johannes Kepler University, Linz, Austria"],"location":"Chiang Mai Thailand","acronym":"iiWAS '20"},"container-title":["Proceedings of the 22nd International Conference on Information Integration and Web-based Applications & Services"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428757.3429146","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428757.3429146","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:32Z","timestamp":1750197752000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428757.3429146"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,30]]},"references-count":54,"alternative-id":["10.1145\/3428757.3429146","10.1145\/3428757"],"URL":"https:\/\/doi.org\/10.1145\/3428757.3429146","relation":{},"subject":[],"published":{"date-parts":[[2020,11,30]]},"assertion":[{"value":"2021-01-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}