{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T23:40:02Z","timestamp":1749771602091,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319502298"},{"type":"electronic","value":"9783319502304"}],"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-50230-4_19","type":"book-chapter","created":{"date-parts":[[2016,11,30]],"date-time":"2016-11-30T13:31:26Z","timestamp":1480512686000},"page":"253-261","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal Model-Based Development in Industrial Automation with Reactive Blocks"],"prefix":"10.1007","author":[{"given":"Peter","family":"Herrmann","sequence":"first","affiliation":[]},{"given":"Jan Olaf","family":"Blech","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,12,1]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-540-27863-4_28","volume-title":"Integration of Software Specification Techniques for Applications in Engineering","author":"N Bauer","year":"2004","unstructured":"Bauer, N., Engell, S., Huuck, R., Lohmann, S., Lukoschus, B., Remelhe, M., Stursberg, O.: Verification of PLC programs given as sequential function charts. In: Ehrig, H., Damm, W., Desel, J., Gro\u00dfe-Rhode, M., Reif, W., Schnieder, E., Westk\u00e4mper, E. (eds.) Integration of Software Specification Techniques for Applications in Engineering. LNCS, vol. 3147, pp. 517\u2013540. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27863-4_28"},{"key":"19_CR2","unstructured":"Bender, K., Katz, M.: PROFIBUS: der Feldbus f\u00fcr die Automation. Hanser (1990)"},{"key":"19_CR3","unstructured":"Bitreactive, A.S.: Reactive Blocks. www.bitreactive.com . Accessed 28 Jan 2016"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-24690-6_6","volume-title":"Software Engineering and Formal Methods","author":"JO Blech","year":"2011","unstructured":"Blech, J.O., Ould Biha, S.: Verification of PLC properties based on formal semantics in Coq. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 58\u201373. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-24690-6_6"},{"key":"19_CR5","unstructured":"Blech, J.O., Schmidt, H.: BeSpaceD: towards a tool framework and methodology for the specification and verification of spatial behavior of distributed software component systems. Technical report 1404.3537. arXiv.org (2014)"},{"key":"19_CR6","unstructured":"Boo, P.: A service tool grows up - ABB ServicePort. In: ABB Review (2015)"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Canet, G., Couffin, S., Lesage, J.J., Petit, A., Schnoebelen, P.: Towards the automatic verification of PLC programs written in instruction list. In: Systems, Man, and Cybernetics, vol. 4, pp. 2449\u20132454. IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884359"},{"key":"19_CR8","unstructured":"Fernandez Adiego, B., Darvas, D., Vinuela, E.B., Tournier, J.C., Bliudze, S., Blech, J.O., Gonzalez Suarez, V.M.: Applying model checking to industrial-sized PLC programs. IEEE Trans. Ind. Inform. 11(6), 1400\u20131410 (2015)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Frey, G., Litz, L.: Formal methods in PLC programming. In: Systems, Man, and Cybernetics, vol. 4, pp. 2431\u20132436. IEEE (2000)","DOI":"10.1109\/ICSMC.2000.884356"},{"key":"19_CR10","unstructured":"Gayet, P., Barillere, R.: UNICOS a framework to build industry like control systems: principles and methodology. In: International Conference on Accelerator and Large Experimental Physics Control Systems, Gen\u00e8ve, Suisse (2005)"},{"key":"19_CR11","unstructured":"Graw, G.: Korrekte Steuerungssoftware. Dissertation, Technische Universit\u00e4t Dortmund (2010) (in German)"},{"key":"19_CR12","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: 39th Annual International Computers, Software and Applications Conference (COMPSAC), pp. 638\u2013646. IEEE Computer (2015)","DOI":"10.1109\/COMPSAC.2015.46"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Harland, J., Blech, J.O., Peake, I., Trodd, L.: Formal behavioural models to facilitate distributed development and commissioning in industrial automation. In: Evaluation of Novel Approaches to Software Engineering, COLAFORM Track (2016)","DOI":"10.5220\/0005928303630369"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"40","DOI":"10.4018\/IJWSR.2016010103","volume":"13","author":"P Herrmann","year":"2016","unstructured":"Herrmann, P., Blech, J.O., Han, F., Schmidt, H.: A model-based toolchain to verify spatial behavior of cyber-physical systems. Int. J. Web Serv. Res. (IJWSR) 13(1), 40\u201352 (2016)","journal-title":"Int. J. Web Serv. Res. (IJWSR)"},{"issue":"2","key":"19_CR15","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/S1389-1286(00)00089-X","volume":"34","author":"P Herrmann","year":"2000","unstructured":"Herrmann, P., Krumm, H.: A framework for modeling transfer protocols. Comput. Netw. 34(2), 317\u2013337 (2000)","journal-title":"Comput. Netw."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Hordvik, S., \u00d8seth, K., Blech, J.O., Herrmann, P.: A methodology for model-based development and safety analysis of transport systems. In: 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE) (2016)","DOI":"10.5220\/0005828800910101"},{"key":"19_CR17","unstructured":"IEC: IEC Standard IEC 61161\u20133. Programmable Controllers \u2013 Programming Languages, 2.0 edn. (01 2003)"},{"key":"19_CR18","unstructured":"Kagermann, H., Wahlster, W., Helbig, J.: Umsetzungsempfehlungen f\u00fcr das Zukunftsprojekt Industrie 4.0. Abschlussbericht des Arbeitskreises Industrie 4, 5 (2013) (in German)"},{"key":"19_CR19","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). doi: 10.1007\/978-3-642-04425-0_44"},{"key":"19_CR20","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\/FORTE -2010. LNCS, vol. 6117, pp. 17\u201331. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-13464-7_3"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1613","DOI":"10.1007\/11914952_41","volume-title":"On the Move to Meaningful Internet Systems 2006: CoopIS, DOA, GADA, and ODBASE","author":"FA Kraemer","year":"2006","unstructured":"Kraemer, F.A., Herrmann, P., Br\u00e6k, R.: Aligning UML 2.0 state machines and temporal logic for the efficient execution of services. In: Meersman, R., Tari, Z. (eds.) OTM 2006. LNCS, vol. 4276, pp. 1613\u20131632. Springer, Heidelberg (2006). doi: 10.1007\/11914952_41"},{"issue":"12","key":"19_CR22","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."},{"key":"19_CR23","unstructured":"Kraemer, F.A., Herrmann, P.: formalizing collaboration-oriented service specifications using temporal logic. In: Networking and Electronic Commerce Research Conference (NAEC), pp. 194\u2013220. ATSMA, Riva del Garda, October 2007"},{"key":"19_CR24","volume-title":"Specifying Systems: The TLA $$^+$$ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: The TLA $$^+$$ Language and Tools for Hardware and Software Engineers. Pearson Education Inc, London (2002)"},{"key":"19_CR25","unstructured":"Object Management Group: OMG Unified Modeling LanguageTM (OMG UML), Superstructure \u2013 Version 2.4.1 (2011). www.omg.org\/spec\/UML\/2.4.1\/Superstructure\/PDF\/ . Accessed 28 Jan 2016"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Rausch, M., Krogh, B.H.: Formal verification of PLC programs. In: American Control Conference, vol. 1, pp. 234\u2013238. IEEE (1998)","DOI":"10.1109\/ACC.1998.694666"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Rushby, J.: Disappearing formal methods. In: High-Assurance Systems Engineering Symposium, pp. 95\u201396. ACM. Albuquerque (2000)","DOI":"10.1109\/HASE.2000.895446"},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-15898-8_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"W Steiner","year":"2010","unstructured":"Steiner, W., Dutertre, B.: SMT-Based formal verification of a TTEthernet synchronization function. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 148\u2013163. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15898-8_10"},{"key":"19_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0031569","volume-title":"Hybrid Systems IV","author":"O Stursberg","year":"1997","unstructured":"Stursberg, O., Kowalewski, S., Hoffmann, I., Preu\u00dfig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol. 1273, pp. 361\u2013377. Springer, Heidelberg (1997). doi: 10.1007\/BFb0031569"},{"key":"19_CR30","volume-title":"Raspberry Pi User Guide","author":"E Upton","year":"2014","unstructured":"Upton, E., Halfacree, G.: Raspberry Pi User Guide. Wiley, Cambridge (2014)"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Vogel-Heuser, B., Witsch, D., Katzke, U.: Automatic code generation from a UML model to IEC 61131\u20133 and system configuration tools. In: International Conference on Control and Automation (ICCA), vol. 2, pp. 1034\u20131039. IEEE (2005)","DOI":"10.1109\/ICCA.2005.1528274"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Vyatkin, V., Hanisch, H.M.: Formal modeling and verification in the software engineering framework of IEC 61499: a way to self-verifying systems. In: Emerging Technologies and Factory Automation (ETFA), vol. 2. IEEE Computer (2001)","DOI":"10.1109\/ETFA.2001.997677"}],"container-title":["Lecture Notes in Computer Science","Software Technologies: Applications and Foundations"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-50230-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T23:11:22Z","timestamp":1749769882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-50230-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319502298","9783319502304"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-50230-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"1 December 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"STAF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Federation of International Conferences on Software Technologies: Applications and Foundations","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vienna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Austria","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":"4 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"staf2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}