{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,14]],"date-time":"2026-07-14T22:13:55Z","timestamp":1784067235244,"version":"3.55.0"},"reference-count":35,"publisher":"Walter de Gruyter GmbH","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,28]]},"abstract":"<jats:title>Zusammenfassung<\/jats:title>\n               <jats:p>Durch zunehmende Agilit\u00e4t im Entwicklungsprozess, k\u00fcrzere Lebenszyklen und sich \u00e4ndernde Kunden- und Gesetzgeberanforderungen m\u00fcssen Produktionssysteme wandlungsf\u00e4hig sein. Aber jede Ver\u00e4nderung des Systemverhaltens muss anschlie\u00dfend auch erneut abgesichert werden. Zur Absicherung sicherheitskritischer Funktionen eignen sich formale Verifikationsmethoden. Allerdings ist hierzu ein hoher Modellierungsaufwand notwendig, was den Einsatz formaler Verifikationsmethoden in der Praxis hemmt. Zudem empfiehlt sich eine \u00dcberpr\u00fcfung der zur formalen Verifikation eingesetzten Modelle. Zur Bew\u00e4ltigung der Herausforderungen f\u00fcr die Absicherung, die eine Rekonfiguration w\u00e4hrend des Betriebs nach sich zieht, werden in diesem Beitrag zwei vielversprechende und sich gegenseitig erg\u00e4nzende Ans\u00e4tze f\u00fcr die lebenszyklus\u00fcbergreifende Absicherung von Produktionssystemen vorgestellt.<\/jats:p>","DOI":"10.1515\/auto-2019-0115","type":"journal-article","created":{"date-parts":[[2019,12,21]],"date-time":"2019-12-21T09:04:45Z","timestamp":1576919085000},"page":"3-14","source":"Crossref","is-referenced-by-count":20,"title":["Formale Methoden f\u00fcr rekonfigurierbare cyber-physische Systeme in der Produktion"],"prefix":"10.1515","volume":"68","author":[{"given":"Marco","family":"Grochowski","sequence":"first","affiliation":[{"name":"Lehrstuhl Informatik 11 \u2013 Embedded Software , RWTH Aachen University , Ahornstra\u00dfe 55 , Aachen , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hendrik","family":"Simon","sequence":"additional","affiliation":[{"name":"Lehrstuhl Informatik 11 \u2013 Embedded Software , RWTH Aachen University , Ahornstra\u00dfe 55 , Aachen , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dimitri","family":"Bohlender","sequence":"additional","affiliation":[{"name":"Lehrstuhl Informatik 11 \u2013 Embedded Software , RWTH Aachen University , Ahornstra\u00dfe 55 , Aachen , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Kowalewski","sequence":"additional","affiliation":[{"name":"Lehrstuhl Informatik 11 \u2013 Embedded Software , RWTH Aachen University , Ahornstra\u00dfe 55 , Aachen , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"L\u00f6cklin","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Automatisierungstechnik und Softwaresysteme , Universit\u00e4t Stuttgart , Pfaffenwaldring 47 , Stuttgart , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Timo","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Automatisierungstechnik und Softwaresysteme , Universit\u00e4t Stuttgart , Pfaffenwaldring 47 , Stuttgart , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nasser","family":"Jazdi","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Automatisierungstechnik und Softwaresysteme , Universit\u00e4t Stuttgart , Pfaffenwaldring 47 , Stuttgart , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Zeller","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Automatisierungstechnik und Softwaresysteme , Universit\u00e4t Stuttgart , Pfaffenwaldring 47 , Stuttgart , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Weyrich","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Automatisierungstechnik und Softwaresysteme , Universit\u00e4t Stuttgart , Pfaffenwaldring 47 , Stuttgart , Deutschland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2019,12,21]]},"reference":[{"key":"2021062112572123777_j_auto-2019-0115_ref_001_w2aab3b7e1027b1b6b1ab2b1b1Aa","unstructured":"Definition von cpps durch vdi\/vde gma fachausschuss 7.20 (cyber physical systems) und 7.21 (industrie 4.0). http:\/\/i40.iosb.fraunhofer.de\/Cyber-Physical Production System (CPPS). Aufgerufen am: 21.08.2019."},{"key":"2021062112572123777_j_auto-2019-0115_ref_002_w2aab3b7e1027b1b6b1ab2b1b2Aa","doi-asserted-by":"crossref","unstructured":"Y. Al-Safi and V. Vyatkin. An ontology-based reconfiguration agent for intelligent mechatronic systems. In V. Ma\u0159\u00edk, V. Vyatkin and A.\u2009W. Colombo, editors, Holonic and Multi-Agent Systems for Manufacturing, pages 114\u2013126, 2007. Springer Berlin Heidelberg, Berlin, Heidelberg.","DOI":"10.1007\/978-3-540-74481-8_12"},{"key":"2021062112572123777_j_auto-2019-0115_ref_003_w2aab3b7e1027b1b6b1ab2b1b3Aa","doi-asserted-by":"crossref","unstructured":"E.\u2009G. Amparore, B. Berthomieu, G. Ciardo, S. Dal-Zilio, F. Gall\u00e0, L. Hillah, F. Hulin-Hubard, P.\u2009G. Jensen, L. Jezequel, F. Kordon, D.\u2009L. Botlan, T. Liebke, J. Meijer, A.\u2009S. Miner, E. Paviot-Adet, J. Srba, Y. Thierry-Mieg, T. van Dijk and K. Wolf. Presentation of the 9th edition of the model checking contest. In Tools and Algorithms for the Construction and Analysis of Systems \u2013 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part III, pages 50\u201368, 2019.","DOI":"10.1007\/978-3-030-17502-3_4"},{"key":"2021062112572123777_j_auto-2019-0115_ref_004_w2aab3b7e1027b1b6b1ab2b1b4Aa","unstructured":"C. Baier and J. Katoen. Principles of model checking. MIT Press, 2008."},{"key":"2021062112572123777_j_auto-2019-0115_ref_005_w2aab3b7e1027b1b6b1ab2b1b5Aa","doi-asserted-by":"crossref","unstructured":"R. Baldoni, E. Coppa, D.\u2009C. D\u2019Elia, C. Demetrescu and I. Finocchi. A survey of symbolic execution techniques. ACM Comput. Surv., 51(3):50:1\u201350:39, 2018.","DOI":"10.1145\/3182657"},{"key":"2021062112572123777_j_auto-2019-0115_ref_006_w2aab3b7e1027b1b6b1ab2b1b6Aa","doi-asserted-by":"crossref","unstructured":"B. Beckert, M. Ulbrich, B. Vogel-Heuser and A. Weigl. Regression verification for programmable logic controller software. In Formal Methods and Software Engineering \u2013 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3\u20135, 2015, Proceedings, pages 234\u2013251, 2015.","DOI":"10.1007\/978-3-319-25423-4_15"},{"key":"2021062112572123777_j_auto-2019-0115_ref_007_w2aab3b7e1027b1b6b1ab2b1b7Aa","unstructured":"K. Bettenhausen and S. Kowalewski. Cyber-physical systems: Chancen und nutzen aus sicht der automation. Technical report, VDI\/VDE GMA, D\u00fcsseldorf, 2013."},{"key":"2021062112572123777_j_auto-2019-0115_ref_008_w2aab3b7e1027b1b6b1ab2b1b8Aa","doi-asserted-by":"crossref","unstructured":"D. Beyer, T.\u2009A. Henzinger and G. Th\u00e9oduloz. Configurable software verification: Concretizing the convergence of model checking and program analysis. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3\u20137, 2007, Proceedings, pages 504\u2013518, 2007.","DOI":"10.1007\/978-3-540-73368-3_51"},{"key":"2021062112572123777_j_auto-2019-0115_ref_009_w2aab3b7e1027b1b6b1ab2b1b9Aa","unstructured":"D. Beyer and T. Lemberger. Software verification: Testing vs. model checking \u2013 A comparative evaluation of the state of the art. In Hardware and Software: Verification and Testing \u2013 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13\u201315, 2017, Proceedings, pages 99\u2013114, 2017."},{"key":"2021062112572123777_j_auto-2019-0115_ref_010_w2aab3b7e1027b1b6b1ab2b1c10Aa","doi-asserted-by":"crossref","unstructured":"S. Biallas, J. Brauer and S. Kowalewski. Arcade.plc: a verification platform for programmable logic controllers. In IEEE\/ACM International Conference on Automated Software Engineering, ASE\u201912, Essen, Germany, September 3\u20137, 2012, pages 338\u2013341, 2012.","DOI":"10.1145\/2351676.2351741"},{"key":"2021062112572123777_j_auto-2019-0115_ref_011_w2aab3b7e1027b1b6b1ab2b1c11Aa","doi-asserted-by":"crossref","unstructured":"D. Bohlender, H. Simon, N. Friedrich, S. Kowalewski and S. Hauck-Stattelmann. Concolic test generation for PLC programs using coverage metrics. In C.\u2009G. Cassandras, A. Giua and Z. Li, editors, 13th International Workshop on Discrete Event Systems, WODES 2016, Xi\u2019an, China, May 30\u2013June 1, 2016, pages 432\u2013437. IEEE, 2016.","DOI":"10.1109\/WODES.2016.7497884"},{"key":"2021062112572123777_j_auto-2019-0115_ref_012_w2aab3b7e1027b1b6b1ab2b1c12Aa","doi-asserted-by":"crossref","unstructured":"G. Frey. Hierarchical design of logic controllers using signal interpreted petri nets. IFAC Proceedings Volumes, 36(6):361\u2013366, 2003.","DOI":"10.1016\/S1474-6670(17)36458-3"},{"key":"2021062112572123777_j_auto-2019-0115_ref_013_w2aab3b7e1027b1b6b1ab2b1c13Aa","doi-asserted-by":"crossref","unstructured":"E. Geisberger and M. Broy. agendaCPS: Integrierte Forschungsagenda Cyber-Physical Systems, volume 1. Springer-Verlag, 2012.","DOI":"10.1007\/978-3-642-29099-2"},{"key":"2021062112572123777_j_auto-2019-0115_ref_014_w2aab3b7e1027b1b6b1ab2b1c14Aa","doi-asserted-by":"crossref","unstructured":"A. Hees and G. Reinhart. Approach for production planning in reconfigurable manufacturing systems. Procedia CIRP, 33:70\u201375, 2015. 9th CIRP Conference on Intelligent Computation in Manufacturing Engineering \u2013 CIRP ICME\u201914.","DOI":"10.1016\/j.procir.2015.06.014"},{"key":"2021062112572123777_j_auto-2019-0115_ref_015_w2aab3b7e1027b1b6b1ab2b1c15Aa","unstructured":"A.\u2009F. Hees. System zur Produktionsplanung f\u00fcr rekonfigurierbare Produktionssysteme. Dissertation, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, 2017."},{"key":"2021062112572123777_j_auto-2019-0115_ref_016_w2aab3b7e1027b1b6b1ab2b1c16Aa","doi-asserted-by":"crossref","unstructured":"E. J\u00e4rvenp\u00e4\u00e4, N. Siltala and M. Lanz. Formal resource and capability descriptions supporting rapid reconfiguration of assembly systems. In 2016 IEEE International Symposium on Assembly and Manufacturing (ISAM), pages 120\u2013125. IEEE, 2016.","DOI":"10.1109\/ISAM.2016.7750724"},{"key":"2021062112572123777_j_auto-2019-0115_ref_017_w2aab3b7e1027b1b6b1ab2b1c17Aa","doi-asserted-by":"crossref","unstructured":"N. Jazdi. Cyber physical systems in the context of industry 4.0. In 2014 IEEE International Conference on Automation, Quality and Testing, Robotics, pages 1\u20134, May 2014.","DOI":"10.1109\/AQTR.2014.6857843"},{"key":"2021062112572123777_j_auto-2019-0115_ref_018_w2aab3b7e1027b1b6b1ab2b1c18Aa","doi-asserted-by":"crossref","unstructured":"E. J\u00e4rvenp\u00e4\u00e4, N. Siltala, O. Hylli and M. Lanz. Capability matchmaking procedure to support rapid configuration and re-configuration of production systems. Procedia Manufacturing, 11:1053\u20131060, 2017. 27th International Conference on Flexible Automation and Intelligent Manufacturing, FAIM2017, 27\u201330 June 2017, Modena, Italy.","DOI":"10.1016\/j.promfg.2017.07.216"},{"key":"2021062112572123777_j_auto-2019-0115_ref_019_w2aab3b7e1027b1b6b1ab2b1c19Aa","doi-asserted-by":"crossref","unstructured":"Y. Koren, X. Gu and W. Guo. Reconfigurable manufacturing systems: Principles, design, and future trends. Frontiers of Mechanical Engineering, 13(2):121\u2013136, Jun 2018.","DOI":"10.1007\/s11465-018-0483-0"},{"key":"2021062112572123777_j_auto-2019-0115_ref_020_w2aab3b7e1027b1b6b1ab2b1c20Aa","unstructured":"S. Kowalewski and K.\u2009D. Bettenhausen. Cyber-physical systems: Chancen und nutzen aus sicht der automation. VDI\/VDE-Gesellschaft Mess-und Automatisierungstechnik, 2013."},{"key":"2021062112572123777_j_auto-2019-0115_ref_021_w2aab3b7e1027b1b6b1ab2b1c21Aa","doi-asserted-by":"crossref","unstructured":"T. Lange, M.\u2009R. Neuh\u00e4u\u00dfer and T. Noll. Speeding up the safety verification of programmable logic controller code. In Hardware and Software: Verification and Testing \u2013 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5\u20137, 2013, Proceedings, pages 44\u201360, 2013.","DOI":"10.1007\/978-3-319-03077-7_4"},{"key":"2021062112572123777_j_auto-2019-0115_ref_022_w2aab3b7e1027b1b6b1ab2b1c22Aa","doi-asserted-by":"crossref","unstructured":"W. Lepuschitz, A. Zoitl, M. Vall\u00e9e and M. Merdan. Toward self-reconfiguration of manufacturing systems using automation agents. IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), 41(1):52\u201369, Jan 2011.","DOI":"10.1109\/TSMCC.2010.2059012"},{"key":"2021062112572123777_j_auto-2019-0115_ref_023_w2aab3b7e1027b1b6b1ab2b1c23Aa","doi-asserted-by":"crossref","unstructured":"J. Matevska. Rekonfiguration komponentenbasierter Softwaresysteme zur Laufzeit. Springer, 2010.","DOI":"10.1007\/978-3-8348-9780-0"},{"key":"2021062112572123777_j_auto-2019-0115_ref_024_w2aab3b7e1027b1b6b1ab2b1c24Aa","doi-asserted-by":"crossref","unstructured":"C. M\u00fcller-Schloer, H. Schmeck and T. Ungerer. Organic computing. Informatik-Spektrum, 35:71\u201373, 04 2012.","DOI":"10.1007\/s00287-012-0599-2"},{"key":"2021062112572123777_j_auto-2019-0115_ref_025_w2aab3b7e1027b1b6b1ab2b1c25Aa","doi-asserted-by":"crossref","unstructured":"H. Simon, N. Friedrich, S. Biallas, S. Hauck-Stattelmann, B. Schlich and S. Kowalewski. Automatic test case generation for PLC programs using coverage metrics. In 20th IEEE Conference on Emerging Technologies & Factory Automation, ETFA 2015, Luxembourg, September 8\u201311, 2015, pages 1\u20134. IEEE, 2015.","DOI":"10.1109\/ETFA.2015.7301602"},{"key":"2021062112572123777_j_auto-2019-0115_ref_026_w2aab3b7e1027b1b6b1ab2b1c26Aa","doi-asserted-by":"crossref","unstructured":"Y. Thierry-Mieg. Symbolic model-checking using its-tools. In Tools and Algorithms for the Construction and Analysis of Systems \u2013 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015, Proceedings, pages 231\u2013237, 2015.","DOI":"10.1007\/978-3-662-46681-0_20"},{"key":"2021062112572123777_j_auto-2019-0115_ref_027_w2aab3b7e1027b1b6b1ab2b1c27Aa","unstructured":"Y. Thierry Mieg. From Symbolic Verification To Domain Specific Languages. Habilitation \u00e0 diriger des recherches, Sorbonne Universit\u00e9, UPMC; Laboratoire d\u2019informatique de Paris 6 [LIP6], Dec. 2016."},{"key":"2021062112572123777_j_auto-2019-0115_ref_028_w2aab3b7e1027b1b6b1ab2b1c28Aa","doi-asserted-by":"crossref","unstructured":"W.\u2009M. Van Der Aalst, N. Lohmann, P. Massuthe, C. Stahl and K. Wolf. Multiparty contracts: Agreeing and implementing interorganizational processes. The Computer Journal, 53(1):90\u2013106, 2010.","DOI":"10.1093\/comjnl\/bxn064"},{"key":"2021062112572123777_j_auto-2019-0115_ref_029_w2aab3b7e1027b1b6b1ab2b1c29Aa","doi-asserted-by":"crossref","unstructured":"B. Vogel-Heuser, A. Fay, I. Schaefer and M. Tichy. Evolution of software in automated production systems: Challenges and research directions. Journal of Systems and Software, 110:54\u201384, 2015.","DOI":"10.1016\/j.jss.2015.08.026"},{"key":"2021062112572123777_j_auto-2019-0115_ref_030_w2aab3b7e1027b1b6b1ab2b1c30Aa","doi-asserted-by":"crossref","unstructured":"M. Weyrich, M. Klein, J.-P. Schmidt, N. Jazdi, K.\u2009D. Bettenhausen, F. Buschmann, C. Rubner, M. Pirker and K. Wurm. Evaluation Model for Assessment of Cyber-Physical Production Systems, pages 169\u2013199. Springer International Publishing, Cham, 2017.","DOI":"10.1007\/978-3-319-42559-7_7"},{"key":"2021062112572123777_j_auto-2019-0115_ref_031_w2aab3b7e1027b1b6b1ab2b1c31Aa","doi-asserted-by":"crossref","unstructured":"J. Yan and V. Vyatkin. Extension of reconfigurability provisions in iec 61499. In 2013 IEEE 18th Conference on Emerging Technologies Factory Automation (ETFA), pages 1\u20137, 09 2013.","DOI":"10.1109\/ETFA.2013.6648026"},{"key":"2021062112572123777_j_auto-2019-0115_ref_032_w2aab3b7e1027b1b6b1ab2b1c32Aa","unstructured":"A. Zeller, N. Jazdi and M. Weyrich. Functional verification of distributed automation systems: Assisting production line operators by an automated model composition. The International Journal of Advanced Manufacturing Technology, pages 1\u201314, 07 2019."},{"key":"2021062112572123777_j_auto-2019-0115_ref_033_w2aab3b7e1027b1b6b1ab2b1c33Aa","doi-asserted-by":"crossref","unstructured":"A. Zeller and M. Weyrich. Component based verification of distributed automation systems based on model composition. Procedia CIRP, 72:352\u2013356, 2018.","DOI":"10.1016\/j.procir.2018.03.183"},{"key":"2021062112572123777_j_auto-2019-0115_ref_034_w2aab3b7e1027b1b6b1ab2b1c34Aa","doi-asserted-by":"crossref","unstructured":"A. Zeller and M. Weyrich. Composition of modular models for verification of distributed automation systems. Procedia Manufacturing, 17:870\u2013877, 2018.","DOI":"10.1016\/j.promfg.2018.10.139"},{"key":"2021062112572123777_j_auto-2019-0115_ref_035_w2aab3b7e1027b1b6b1ab2b1c35Aa","doi-asserted-by":"crossref","unstructured":"X. Zheng and C. Julien. Verification and validation in cyber physical systems: Research challenges and a way forward. In 1st IEEE\/ACM International Workshop on Software Engineering for Smart Cyber-Physical Systems, SEsCPS 2015, Florence, Italy, May 17, 2015, pages 15\u201318, 2015.","DOI":"10.1109\/SEsCPS.2015.11"}],"container-title":["at - Automatisierungstechnik"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.degruyter.com\/view\/journals\/auto\/68\/1\/article-p3.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/auto-2019-0115\/xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/auto-2019-0115\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,6,21]],"date-time":"2021-06-21T19:10:11Z","timestamp":1624302611000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.degruyter.com\/document\/doi\/10.1515\/auto-2019-0115\/html"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,21]]},"references-count":35,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2019,12,21]]},"published-print":{"date-parts":[[2020,1,28]]}},"alternative-id":["10.1515\/auto-2019-0115"],"URL":"https:\/\/doi.org\/10.1515\/auto-2019-0115","relation":{},"ISSN":["2196-677X","0178-2312"],"issn-type":[{"value":"2196-677X","type":"electronic"},{"value":"0178-2312","type":"print"}],"subject":[],"published":{"date-parts":[[2019,12,21]]}}}