{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:57Z","timestamp":1740099117336,"version":"3.37.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319951614"},{"type":"electronic","value":"9783319951621"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-95162-1_6","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T04:15:34Z","timestamp":1530591334000},"page":"80-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Towards the Modular Specification and Validation of Cyber-Physical Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5035-3005","authenticated-orcid":false,"given":"Andre","family":"Metelo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1296-2007","authenticated-orcid":false,"given":"Christiano","family":"Braga","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3874-784X","authenticated-orcid":false,"given":"Diego","family":"Brand\u00e3o","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Akella, R., McMillin, B.: Model-cheking BNDC properties in cyber-physical systems. In: Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference COMPSAC 2009, pp. 660\u2013663. IEEE (2009)","DOI":"10.1109\/COMPSAC.2009.101"},{"key":"6_CR2","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"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\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"issue":"2","key":"6_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"6_CR5","volume-title":"Finite Transition Systems: Semantics of Communicating Systems","author":"A Arnold","year":"1994","unstructured":"Arnold, A.: Finite Transition Systems: Semantics of Communicating Systems. Prentice Hall International (UK) Ltd., Hertfordshire (1994)"},{"key":"6_CR6","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.: Designing and verifying distributed cyber-physical systems using multirate pals: an airplane turning control system case study. Sci. Comput. Program. (2015). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0167642314004109"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Bae, K., \u00d6lveczky, P., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, pp. 145\u2013154. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2883817.2883849","DOI":"10.1145\/2883817.2883849"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Broman, D., Lee, E., Tripakis, S., Torngren, M.: Viewpoints, formalisms, languages, and tools for cyber-physical systems. In: Proceedings of the 6th International Workshop on Multi-Paradigm Modeling, pp. 49\u201354 (2012)","DOI":"10.1145\/2508443.2508452"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2000367.2000368","volume":"8","author":"L Bu","year":"2011","unstructured":"Bu, L., Wang, Q., Chen, X.: Toward online hybrid systems model checking of cyber-physical systems time-bounded short-run behavior. ACM SIGBED Rev. 8, 7\u201310 (2011)","journal-title":"ACM SIGBED Rev."},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1987, pp. 178\u2013188. ACM, New York (1987). https:\/\/doi.org\/10.1145\/41625.41641","DOI":"10.1145\/41625.41641"},{"issue":"10","key":"6_CR12","doi-asserted-by":"publisher","first-page":"1263","DOI":"10.1109\/82.799677","volume":"46","author":"E Christen","year":"1999","unstructured":"Christen, E., Bakalar, K.: VHDL-AMS-a hardware description language for analog and mixed-signal applications. IEEE Trans. Circ. Syst. II: Analog Digit. Sig. Process. 46(10), 1263\u20131272 (1999). See also: IEEE Trans. Circ. Syst. II: Express Briefs","journal-title":"IEEE Trans. Circ. Syst. II: Analog Digit. Sig. Process."},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"6_CR14","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Maude Manual (Version 2.7.1). SRI International (2016)"},{"key":"6_CR15","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/978-3-642-59615-5_13"},{"key":"6_CR16","volume-title":"Spin Model Checker, the: Primer and Reference Manual","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: Spin Model Checker, the: Primer and Reference Manual. Addison-Wesley Professional, Boston (2003)"},{"key":"6_CR17","unstructured":"Lygeros, J., Tomlin, C., Sastry, S.: Hybrid Systems: Modeling, Analysis and Control. University of California (2008)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-319-46520-3_10","volume-title":"Automated Technology for Verification and Analysis","author":"\u00d3 Mart\u00edn","year":"2016","unstructured":"Mart\u00edn, \u00d3., Verdejo, A., Mart\u00ed-Oliet, N.: Synchronous products of rewrite systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 141\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_10"},{"issue":"1","key":"6_CR19","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90182-F","journal-title":"Theor. Comput. Sci."},{"key":"6_CR20","unstructured":"Moura, L., Owre, S., Shankar, N.: The SAL language manual. SRI International (2003)"},{"key":"6_CR21","unstructured":"\u00d6lveczky, P.: Real-Time Maude 2.3 Manual. University of Oslo (2007). http:\/\/heim.ifi.uio.no\/peterol\/RealTimeMaude\/"},{"key":"6_CR22","series-title":"Undergraduate Topics in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-6687-0","volume-title":"Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude","author":"P \u00d6lveczky","year":"2018","unstructured":"\u00d6lveczky, P.: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Undergraduate Topics in Computer Science. Springer, London (2018). https:\/\/doi.org\/10.1007\/978-1-4471-6687-0"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/S0304-3975(01)00363-2","volume":"285","author":"PC \u00d6lveczky","year":"2002","unstructured":"\u00d6lveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359\u2013405 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00363-2","journal-title":"Theor. Comput. Sci."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Shafi, Q.: Cyber physical systems security: a brief survey. In: 12th International Conference on Computational Science and Its Applications (ICCSA), Salvador, Brazil, pp. 146\u2013150. IEEE (2012)","DOI":"10.1109\/ICCSA.2012.36"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Smith, D.: VHDL and Verilog compared and contrasted-plus modeled example written in VHDL, Verilog and C. In: Proceedings of the 33rd Annual Design Automation Conference (1996)","DOI":"10.1145\/240518.240664"},{"key":"6_CR26","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133\u2013191. MIT Press, Cambridge (1990). http:\/\/dl.acm.org\/citation.cfm?id=114891.114895"},{"key":"6_CR27","doi-asserted-by":"publisher","unstructured":"Zhang, L., Hu, W., Qu, W., Guo, Y., Li, S.: A formal approach to verify parameterized protocols in mobile cyber-physical systems. Mob. Inf. Syst. (2017). https:\/\/doi.org\/10.1155\/2017\/5731678","DOI":"10.1155\/2017\/5731678"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2018"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95162-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T04:09:23Z","timestamp":1571544563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95162-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319951614","9783319951621"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95162-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}