{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:51:07Z","timestamp":1740099067203,"version":"3.37.3"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319955810"},{"type":"electronic","value":"9783319955827"}],"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-95582-7_10","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T10:31:17Z","timestamp":1531305077000},"page":"165-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["IPL: An Integration Property Language for Multi-model Cyber-physical Systems"],"prefix":"10.1007","author":[{"given":"Ivan","family":"Ruchkin","sequence":"first","affiliation":[]},{"given":"Joshua","family":"Sunshine","sequence":"additional","affiliation":[]},{"given":"Grant","family":"Iraci","sequence":"additional","affiliation":[]},{"given":"Bradley","family":"Schmerl","sequence":"additional","affiliation":[]},{"given":"David","family":"Garlan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10270-015-0469-x","volume":"15","author":"PJ Mosterman","year":"2016","unstructured":"Mosterman, P.J., Zander, J.: Cyber-physical systems challenges: a needs analysis for collaborating embedded software systems. Softw. Syst. Model. 15(1), 5\u201316 (2016)","journal-title":"Softw. Syst. Model."},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-642-16265-7_2","volume-title":"Integrated Formal Methods","author":"J Fitzgerald","year":"2010","unstructured":"Fitzgerald, J., Larsen, P.G., Pierce, K., Verhoef, M., Wolff, S.: Collaborative modelling and co-simulation in the development of dependable embedded systems. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 12\u201326. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16265-7_2"},{"key":"10_CR3","unstructured":"Valukas, A.: Report to board of directors of general motors company regarding ignition switch recalls. Jenner & Block, Technical report (2014)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Sztipanovits, J., Koutsoukos, X., Karsai, G., Kottenstette, N., Antsaklis, P., Gupta, V., Goodwine, B., Baras, J., Wang, S.: Toward a science of cyber-physical system integration. In: Proceedings of the IEEE (2011)","DOI":"10.1109\/JPROC.2011.2161529"},{"key":"10_CR5","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":"10_CR6","unstructured":"Dijkman, R.M.: Consistency in multi-viewpoint architectural design. Ph.D. thesis, Telematica Instituut, Enschede, The Netherlands (2006)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Maoz, S., Ringert, J.O., Rumpe, B.: Synthesis of component and connector models from crosscutting structural views. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2013, New York, NY, USA, pp. 444\u2013454. ACM (2013)","DOI":"10.1145\/2491411.2491414"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-54862-8_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Reineke","year":"2014","unstructured":"Reineke, J., Tripakis, S.: Basic problems in multi-view modeling. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 217\u2013232. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_15"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Bhave, A.: Multi-view consistency in architectures for cyber-physical systems. Ph.D. thesis, Carnegie Mellon University, December 2011","DOI":"10.1109\/ICCPS.2011.17"},{"key":"10_CR10","volume-title":"Dynamic Programming and Markov Processes","author":"RA Howard","year":"1960","unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. Technology Press of the Massachusetts Institute of Technology, Cambridge (1960)"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72522-0_6"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Bhave, A., Krogh, B., Garlan, D., Schmerl, B.: View consistency in architectures for cyber-physical systems. In: IEEE\/ACM International Conference on Cyber-Physical Systems (ICCPS) (2011)","DOI":"10.1109\/ICCPS.2011.17"},{"issue":"10","key":"10_CR13","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1109\/32.328995","volume":"20","author":"B Nuseibeh","year":"1994","unstructured":"Nuseibeh, B., Kramer, J., Finkelstein, A.: A framework for expressing the relationships between multiple views in requirements specification. IEEE Trans. Softw. Eng. 20(10), 760\u2013773 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR14","unstructured":"Egyed, A.F.: Heterogeneous view integration and its automation. Ph.D. thesis, University of Southern California (2000)"},{"issue":"8","key":"10_CR15","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"10_CR16","series-title":"Advances in Formal Methods","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Advances in Formal Methods, vol. 1. Springer, New York (2000). https:\/\/doi.org\/10.1007\/978-1-4615-5265-9"},{"key":"10_CR17","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)","edition":"1"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-540-87785-1_5","volume-title":"Software Technologies for Embedded and Ubiquitous Systems","author":"G Karsai","year":"2008","unstructured":"Karsai, G., Sztipanovits, J.: Model-integrated development of cyber-physical systems. In: Brinkschulte, U., Givargis, T., Russo, S. (eds.) SEUS 2008. LNCS, vol. 5287, pp. 46\u201354. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87785-1_5"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Ruchkin, I.: Integration beyond components and models: research challenges and directions. In: Proceedings of the Third Workshop on Architecture Centric Virtual Integration (ACVI), Venice, Italy, pp. 8\u201311 (2016)","DOI":"10.1109\/ACVI.2016.8"},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/52.469759","volume":"12","author":"P Kruchten","year":"1995","unstructured":"Kruchten, P.: The 4+1 view model of architecture. IEEE Softw. 12, 42\u201350 (1995)","journal-title":"IEEE Softw."},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Rajhans, A., Bhave, A., Loos, S., Krogh, B., Platzer, A., Garlan, D.: Using parameters in architectural views to support heterogeneous design and verification. In: Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC) (2011)","DOI":"10.1109\/CDC.2011.6161408"},{"key":"10_CR22","unstructured":"Marinescu, R.: Model-driven analysis and verification of automotive embedded systems. Ph.D. thesis, Maladaren University (2016)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Vanherpen, K., Denil, J., David, I., De Meulenaere, P., Mosterman, P.J., Torngren, M., Qamar, A., Vangheluwe, H.: Ontological reasoning for consistency in the design of cyber-physical systems, pp. 1\u20138. IEEE, April 2016","DOI":"10.1109\/CPPS.2016.7483922"},{"key":"10_CR24","doi-asserted-by":"publisher","first-page":"745","DOI":"10.1016\/j.mechatronics.2013.11.013","volume":"24","author":"M Torngren","year":"2013","unstructured":"Torngren, M., Qamar, A., Biehl, M., Loiret, F., El-khoury, J.: Integrating viewpoints in the development of mechatronic products. Mechatronics 24, 745\u2013762 (2013)","journal-title":"Mechatronics"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Rajhans, A., Krogh, B.H.: Heterogeneous verification of cyber-physical systems using behavior relations. In: Proceedings of the 15th ACM Conference on Hybrid Systems: Computation and Control (HSCC), New York, NY, USA, pp. 35\u201344. ACM (2012)","DOI":"10.1145\/2185632.2185641"},{"key":"10_CR26","volume-title":"System Design, Modeling, and Simulation using Ptolemy II","author":"EA Lee","year":"2014","unstructured":"Lee, E.A., Neuendorffer, S., Zhou, G.: System Design, Modeling, and Simulation using Ptolemy II. Ptolemy.org, Berkeley (2014)"},{"issue":"6","key":"10_CR27","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1109\/MC.2014.147","volume":"47","author":"B Combemale","year":"2014","unstructured":"Combemale, B., Deantoni, J., Baudry, B., France, R., Jezequel, J.M., Gray, J.: Globalizing modeling languages. Computer 47(6), 68\u201371 (2014)","journal-title":"Computer"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-54848-2_16","volume-title":"From Programs to Systems. The Systems perspective in Computing","author":"J Sztipanovits","year":"2014","unstructured":"Sztipanovits, J., Bapty, T., Neema, S., Howard, L., Jackson, E.: OpenMETA: a model- and component-based design tool chain for cyber-physical systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 235\u2013248. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54848-2_16"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/978-3-642-41533-3_29","volume-title":"Model-Driven Engineering Languages and Systems","author":"G Simko","year":"2013","unstructured":"Simko, G., Lindecker, D., Levendovszky, T., Neema, S., Sztipanovits, J.: Specification of cyber-physical components with formal semantics \u2013 integration and composition. In: Moreira, A., Sch\u00e4tz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 471\u2013487. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41533-3_29"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Ruchkin, I., de Niz, D., Chaki, S., Garlan, D.: Contract-based integration of cyber-physical analyses. In: Proceedings of the International Conference on Embedded Software (EMSOFT), New York, NY, USA, pp. 23:1\u201323:10. ACM (2014)","DOI":"10.21236\/ADA610847"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-32940-1_14","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"A Costa Da","year":"2012","unstructured":"Da Costa, A., Laroussinie, F., Markey, N.: Quantified CTL: expressiveness and model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 177\u2013192. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_14"},{"key":"10_CR32","volume-title":"The Classical Decision Problem","author":"E Borger","year":"2001","unstructured":"Borger, E., Gradel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (2001)"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357, October 1977","DOI":"10.1109\/SFCS.1977.32"},{"key":"10_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"key":"10_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-540-73595-3_25","volume-title":"Automated Deduction \u2013 CADE-21","author":"S Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 362\u2013378. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_25"},{"issue":"2","key":"10_CR36","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/s10270-009-0130-7","volume":"10","author":"A Cimatti","year":"2009","unstructured":"Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Formalizing requirements with object models and temporal constraints. Softw. Syst. Model. 10(2), 147\u2013160 (2009)","journal-title":"Softw. Syst. Model."},{"issue":"4","key":"10_CR37","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.2307\/2275807","volume":"61","author":"DM Gabbay","year":"1996","unstructured":"Gabbay, D.M.: Fibred semantics and the weaving of logics part 1: modal and intuitionistic logics. J. Symb. Log. 61(4), 1057\u20131120 (1996)","journal-title":"J. Symb. Log."},{"key":"10_CR38","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2013.07.012","volume":"503","author":"S Konur","year":"2013","unstructured":"Konur, S., Fisher, M., Schewe, S.: Combined model checking for temporal, probabilistic, and real-time logics. Theor. Comput. Sci. 503, 61\u201388 (2013)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"10_CR39","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"2","key":"10_CR40","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"10_CR41","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR42","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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR43","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"10_CR44","volume-title":"Documenting Software Architectures: Views and Beyond","author":"P Clements","year":"2010","unstructured":"Clements, P., Bachmann, F., Bass, L., Garlan, D., Ivers, J., Little, R., Merson, P., Nord, R., Stafford, J.: Documenting Software Architectures: Views and Beyond, 2nd edn. Addison-Wesley Professional, Boston (2010)","edition":"2"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Shoham, S., Meshman, Y.: SMT-based Verification of Parameterized Systems. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, New York, NY, USA, pp. 338\u2013348. ACM (2016)","DOI":"10.1145\/2950290.2950330"},{"key":"10_CR46","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-74105-3"},{"key":"10_CR47","unstructured":"Ruchkin, I., Sunshine, J., Iraci, G., Schmerl, B., Garlan, D.: Appendix for IPL: an integration property language for multi-model cyber-physical systems (2018). http:\/\/acme.able.cs.cmu.edu\/pubs\/uploads\/pdf\/fm2018-appendix.pdf"},{"key":"10_CR48","volume-title":"Case Study Research: Design and Methods","author":"RK Yin","year":"2008","unstructured":"Yin, R.K.: Case Study Research: Design and Methods, 4th edn. Sage Publications Inc., Thousand Oaks (2008)","edition":"4"},{"key":"10_CR49","volume-title":"Programming Robots with ROS: A Practical Introduction to the Robot Operating System","author":"M Quigley","year":"2015","unstructured":"Quigley, M., Gerkey, B., Smart, W.D.: Programming Robots with ROS: A Practical Introduction to the Robot Operating System, 1st edn. O\u2019Reilly Media, Sebastopol (2015)","edition":"1"},{"key":"10_CR50","doi-asserted-by":"crossref","unstructured":"Feiler, P.H., Gluch, D.P., Hudak, J.J.: The architecture analysis & design language (AADL): an introduction. Technical report CMU\/SEI-2006-TN-011, Software Engineering Institute, Carnegie Mellon University (2006)","DOI":"10.21236\/ADA455842"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T12:29:17Z","timestamp":1571574557000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}