{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T01:56:58Z","timestamp":1725847018809},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662492239"},{"type":"electronic","value":"9783662492246"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-49224-6_5","type":"book-chapter","created":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T08:35:44Z","timestamp":1452501344000},"page":"43-52","source":"Crossref","is-referenced-by-count":2,"title":["Behavioral Types for Component-Based Development of Cyber-Physical Systems"],"prefix":"10.1007","author":[{"given":"Jan Olaf","family":"Blech","sequence":"first","affiliation":[]},{"given":"Peter","family":"Herrmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,12]]},"reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"5_CR2","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/j.scico.2011.10.007","volume":"78","author":"L Acciai","year":"2013","unstructured":"Acciai, L., Boreale, M., Zavattaro, G.: Behavioural contracts with request-response operations. Sci. Comput. Program. 78(2), 248\u2013267 (2013)","journal-title":"Sci. Comput. Program."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Symposium on Foundations of Software Engineering. ACM (2001)","DOI":"10.1145\/503225.503226"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-39656-7_2","volume-title":"Formal Methods for Components and Objects","author":"F Arbab","year":"2003","unstructured":"Arbab, F.: Abstract behavior types: a foundation model for components and their composition. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 33\u201370. Springer, Heidelberg (2003)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-32759-9_9","volume-title":"FM 2012: Formal Methods","author":"H Barringer","year":"2012","unstructured":"Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68\u201384. Springer, Heidelberg (2012)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-24622-0_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Barringer","year":"2004","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-642-20398-5_3","volume-title":"NASA Formal Methods","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M.: The theory and practice of SALT. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 13\u201340. Springer, Heidelberg (2011)"},{"issue":"7","key":"5_CR8","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/2.774917","volume":"32","author":"A Beugnard","year":"1999","unstructured":"Beugnard, A., J\u00e9z\u00e9quel, J.-M., Plouzeau, N., Watkins, D.: Making components contract aware. Computer 32(7), 38\u201345 (1999)","journal-title":"Computer"},{"key":"5_CR9","unstructured":"Blech, J.O.: Ensuring OSGi component based properties at runtime with behavioral types. In: 10th Workshop on Model Design, Verification and Validation Integrating Verification and Validation in MDE (2013)"},{"key":"5_CR10","unstructured":"Blech, J.O.: Towards a Formalization of the OSGi Component Framework (2012). \n                      arxiv.org\/abs\/1208.2563v1"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Blech, J.O.: Towards a framework for behavioral specifications of OSGi components. In: 10th International Workshop on Formal Engineering Approaches to Software Components and Architectures. Electronic Proceedings in Theoretical Computer Science (2013)","DOI":"10.4204\/EPTCS.108.6"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-642-34026-0_30","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"JO Blech","year":"2012","unstructured":"Blech, J.O., Falcone, Y., Rue\u00df, H., Sch\u00e4tz, B.: Behavioral specification based runtime monitors for OSGi services. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol. 7609, pp. 405\u2013419. Springer, Heidelberg (2012)"},{"key":"5_CR13","unstructured":"Blech, J.O., Rue\u00df, H., Sch\u00e4tz, B.: On Behavioral Types for OSGi: From Theory to Implementation (2013). \n                      arxiv.org\/abs\/1306.6115"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Blech, J.O., Sch\u00e4tz, B.: Towards a formal foundation of behavioral types for UML state-machines. In: 5th International Workshop UML and Formal Methods, Paris. ACM SIGSOFT Software Engineering Notes (2012)","DOI":"10.1145\/2237796.2237814"},{"key":"5_CR15","unstructured":"Blech, J.O., Schmidt, H.: Towards modeling and checking the spatial and interaction behavior of widely distributed systems. In: Improving Systems and Software Engineering Conference, Melbourne (2013)"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Bliudze, S., Mavridou, A., Szymanek, R., Zolotukhina, A.: Coordination of software components with BIP: application to OSGi. In: 6th International Workshop on Modeling in Software Engineering. ACM (2014)","DOI":"10.1145\/2593770.2593777"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10009-010-0183-5","volume":"14","author":"E Bodden","year":"2012","unstructured":"Bodden, E., Hendren, L.: The clara framework for hybrid typestate analysis. Int. J. Softw. Tools Technol. Transf. (STTT) 14, 307\u2013326 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1017\/S0960129509007658","volume":"19","author":"M Bravetti","year":"2009","unstructured":"Bravetti, M., Zavattaro, G.: A theory of contracts for strong service compliance. Math. Struct. Comput. Sci. 19(3), 601\u2013638 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Cao, T.D., Phan-Quang, T.T., F\u00e9lix, P., Castanet, R.: Automated runtime verification for web services. In: International Conference on Web Services. IEEE Computer Society (2010)","DOI":"10.1109\/ICWS.2010.19"},{"issue":"5","key":"5_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1538917.1538920","volume":"31","author":"G Castagna","year":"2009","unstructured":"Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Tran. Program. Lang. Syst. 31(5), 1\u201361 (2009)","journal-title":"ACM Tran. Program. Lang. Syst."},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-642-24431-5_3","volume-title":"Formal Methods for Industrial Critical Systems","author":"N Cata\u00f1o","year":"2011","unstructured":"Cata\u00f1o, N., Ahmed, I.: Lightweight verification of a multi-task threaded server: a case study with the plural tool. In: Sala\u00fcn, G., Sch\u00e4tz, B. (eds.) FMICS 2011. LNCS, vol. 6959, pp. 6\u201320. Springer, Heidelberg (2011)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-28872-2_5","volume-title":"Fundamental Approaches to Software Engineering","author":"JL Fiadeiro","year":"2012","unstructured":"Fiadeiro, J.L., Lopes, A.: Consistency of service composition. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering. LNCS, vol. 7212, pp. 63\u201377. Springer, Heidelberg (2012)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Gan, Y., Chechik, M., Nejati, S., Bennett, J., O\u2019Farrell, B., Waterhouse, J.: Runtime monitoring of web service conversations. In: 2007 Conference of the Center for Advanced Studies on Collaborative Research. ACM (2007)","DOI":"10.1145\/1321211.1321217"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1109\/MC.2010.76","volume":"43","author":"S Hall\u00e9","year":"2010","unstructured":"Hall\u00e9, S., Bultan, T., Hughes, G., Alkhalaf, M., Villemaire, R.: Runtime verification of web service interface contracts. Computer 43, 59\u201366 (2010)","journal-title":"Computer"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Hamlen, K.W., Morrisett, G., Schneider, F.B.: Certified in-lined reference monitoring on.NET. In: 2006 Workshop on Programming languages and Analysis for Security. ACM (2006)","DOI":"10.1145\/1134744.1134748"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Han, F., Blech, J.O., Herrmann, P., Schmidt, H.: Model-based engineering and analysis of space-aware systems communicating via IEEE 802.11. In: To appear in 39th Annual International Computers, Software & Applications Conference (COMPSAC). IEEE Computer (2015)","DOI":"10.1109\/COMPSAC.2015.46"},{"issue":"3","key":"5_CR28","doi-asserted-by":"publisher","first-page":"16:1","DOI":"10.1145\/2187671.2187678","volume":"44","author":"J Hatcliff","year":"2012","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). Article 16","journal-title":"ACM Comput. Surv."},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/3-540-44875-6_6","volume-title":"Trust Management","author":"P Herrmann","year":"2003","unstructured":"Herrmann, P.: Trust-based protection of software component users and designers. In: Nixon, P., Terzis, S. (eds.) iTrust 2003. LNCS, vol. 2692, pp. 75\u201390. Springer, Heidelberg (2003)"},{"key":"5_CR30","unstructured":"Herrmann, P., Blech, J.O., Han, F., Schmidt, H.: A model-based toolchain to verify spatial behavior of cyber-physical systems. In: 2014 Asia-Pacific Services Computing Conference (APSCC). IEEE Computer (2014)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-642-04425-0_44","volume-title":"Model Driven Engineering Languages and Systems","author":"FA Kraemer","year":"2009","unstructured":"Kraemer, F.A., Herrmann, P.: Automated encapsulation of UML activities for incremental development and verification. In: Sch\u00fcrr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 571\u2013585. Springer, Heidelberg (2009)"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-13464-7_3","volume-title":"Formal Techniques for Distributed Systems","author":"FA Kraemer","year":"2010","unstructured":"Kraemer, F.A., Herrmann, P.: Reactive semantics for distributed UML activities. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010, Part II. LNCS, vol. 6117, pp. 17\u201331. Springer, Heidelberg (2010)"},{"issue":"12","key":"5_CR34","doi-asserted-by":"publisher","first-page":"2068","DOI":"10.1016\/j.jss.2009.06.057","volume":"82","author":"FA Kraemer","year":"2009","unstructured":"Kraemer, F.A., Sl\u00e5tten, V., Herrmann, P.: Tool support for the rapid composition, analysis and implementation of reactive services. J. Syst. Softw. 82(12), 2068\u20132080 (2009)","journal-title":"J. Syst. Softw."},{"issue":"3","key":"5_CR35","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/s00165-004-0043-8","volume":"16","author":"EA Lee","year":"2004","unstructured":"Lee, E.A., Xiong, Y.: A behavioral type system and its application in ptolemy II. Formal Aspects Comput. 16(3), 210\u2013237 (2004)","journal-title":"Formal Aspects Comput."},{"issue":"10","key":"5_CR36","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \"design by contract\". Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10009-011-0198-6","volume":"14","author":"PO Meredith","year":"2011","unstructured":"Meredith, P.O., Jin, D., Griffith, D., Chen, F., Ro\u015fu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tech. Technol. Transfer 14, 249\u2013289 (2011)","journal-title":"Int. J. Softw. Tech. Technol. Transfer"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Prehofer, C.: Behavioral refinement and compatibility of statechart extensions. In: Formal Engineering Approaches to Software Components and Architectures. Electronic Notes in Theoretical Computer Science (2012)","DOI":"10.1016\/j.entcs.2013.04.006"},{"key":"5_CR39","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3, 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"issue":"12","key":"5_CR40","first-page":"1","volume":"3","author":"O Shaer","year":"2010","unstructured":"Shaer, O., Hornecker, E.: Tangible user interfaces: past, present, and future directions. Found. Trends Hum. Comput. Inter. 3(12), 1\u2013137 (2010)","journal-title":"Found. Trends Hum. Comput. Inter."},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/978-3-642-25106-1_6","volume-title":"On the Move to Meaningful Internet Systems: OTM 2011","author":"F Souza","year":"2011","unstructured":"Souza, F., Lopes, D., Gama, K., Rosa, N., Lima, R.: Dynamic event-based monitoring in a SOA environment. In: Meersman, R., et al. (eds.) OTM 2011, Part II. LNCS, vol. 7045, pp. 498\u2013506. Springer, Heidelberg (2011)"},{"key":"5_CR42","unstructured":"Spichkova, M., Blech, J.O., Herrmann, P., Schmidt, H.: Modeling spatial aspects of safety-critical systems with FOCUS\n                      \n                        \n                      \n                      $$^{ST}$$\n                      \n                        \n                          \n                            \n                            \n                              S\n                              T\n                            \n                          \n                        \n                      \n                    . In: Model-Driven Engineering, Verification, and Validation in MDE, Satellite Event of MoDELS2014, CUR-WS Proceedings, vol. 1235, pp. 49\u201358, Valencia (2014)"},{"key":"5_CR43","volume-title":"Component Software - Beyond Object Oriented Programming","author":"C Szyperski","year":"1997","unstructured":"Szyperski, C.: Component Software - Beyond Object Oriented Programming. Addison-Wesley Longman, New York (1997)"},{"key":"5_CR44","doi-asserted-by":"crossref","unstructured":"Wenger, M., Blech, J.O., Zoitl, A.: Behavioral type-based monitoring for IEC 61499. To appear in Emerging Technologies and Factory Automation (ETFA). IEEE (2015)","DOI":"10.1109\/ETFA.2015.7301447"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49224-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T09:17:40Z","timestamp":1559380660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49224-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662492239","9783662492246"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49224-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}