{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:32:12Z","timestamp":1750221132711,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,14]],"date-time":"2018-10-14T00:00:00Z","timestamp":1539475200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,14]]},"DOI":"10.1145\/3270112.3275334","type":"proceedings-article","created":{"date-parts":[[2018,10,5]],"date-time":"2018-10-05T12:09:14Z","timestamp":1538741354000},"page":"150-155","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A modular approach to integrate verification tools in model based development"],"prefix":"10.1145","author":[{"given":"Sudeep","family":"Kanav","sequence":"first","affiliation":[{"name":"fortiss GmbH"}]}],"member":"320","published-online":{"date-parts":[[2018,10,14]]},"reference":[{"volume-title":"d.}. Atelier B","key":"e_1_3_2_1_1_1","unstructured":"{n. d.}. Atelier B . http:\/\/www.atelierb.eu\/en\/. http:\/\/www.atelierb.eu\/en\/ Accessed: 2018-04-24. {n. d.}. Atelier B. http:\/\/www.atelierb.eu\/en\/. http:\/\/www.atelierb.eu\/en\/ Accessed: 2018-04-24."},{"key":"e_1_3_2_1_2_1","unstructured":"{n. d.}. BTC Embedded Validator. https:\/\/www.btc-es.de\/en\/products\/btc-embeddedvalidator.html Accessed: 2018-04-24.  {n. d.}. BTC Embedded Validator. https:\/\/www.btc-es.de\/en\/products\/btc-embeddedvalidator.html Accessed: 2018-04-24."},{"volume-title":"d.}. cbmc - Bounded Model Checker for C","key":"e_1_3_2_1_3_1","unstructured":"{n. d.}. cbmc - Bounded Model Checker for C . http:\/\/www.cprover.org\/cbmc\/ Accessed: 2017-04-19. {n. d.}. cbmc - Bounded Model Checker for C. http:\/\/www.cprover.org\/cbmc\/ Accessed: 2017-04-19."},{"key":"e_1_3_2_1_4_1","unstructured":"{n. d.}. dezyne. http:\/\/www.verum.com\/\/.  {n. d.}. dezyne. http:\/\/www.verum.com\/\/."},{"key":"e_1_3_2_1_5_1","unstructured":"{n. d.}. FASTEN. https:\/\/github.com\/mbeddr\/mbeddr.formal Accessed: 2018-07-08.  {n. d.}. FASTEN. https:\/\/github.com\/mbeddr\/mbeddr.formal Accessed: 2018-07-08."},{"key":"e_1_3_2_1_6_1","unstructured":"{n.d.}. GEMOC Initiative. http:\/\/gemoc.org\/index.html. Accessed: 2018-07-04.  {n.d.}. GEMOC Initiative. http:\/\/gemoc.org\/index.html. Accessed: 2018-07-04."},{"key":"e_1_3_2_1_7_1","unstructured":"{n.d.}. IETS3 + CELT. https:\/\/www.fortiss.org\/en\/research\/projects\/iets3_celt\/. Accessed: 2018-07-04.  {n.d.}. IETS3 + CELT. https:\/\/www.fortiss.org\/en\/research\/projects\/iets3_celt\/. Accessed: 2018-07-04."},{"key":"e_1_3_2_1_8_1","unstructured":"{n. d.}. MPS - Meta Programming System. https:\/\/www.jetbrains.com\/mps\/.  {n. d.}. MPS - Meta Programming System. https:\/\/www.jetbrains.com\/mps\/."},{"key":"e_1_3_2_1_9_1","unstructured":"{n. d.}. OCRA: Othello Contracts Refinement Analysis Version 1.3.  {n. d.}. OCRA: Othello Contracts Refinement Analysis Version 1.3."},{"key":"e_1_3_2_1_10_1","unstructured":"{n. d.}. Simulink Design Verifier. https:\/\/www.mathworks.com\/products\/sldesignverifier.html Accessed: 2018-04-24.  {n. d.}. Simulink Design Verifier. https:\/\/www.mathworks.com\/products\/sldesignverifier.html Accessed: 2018-04-24."},{"key":"e_1_3_2_1_11_1","unstructured":"{n. d.}. The TLA Home Page. https:\/\/lamport.azurewebsites.net\/tla\/tla.html Accessed: 2018-04-22.  {n. d.}. The TLA Home Page. https:\/\/lamport.azurewebsites.net\/tla\/tla.html Accessed: 2018-04-22."},{"key":"e_1_3_2_1_12_1","unstructured":"2012-2017. etrice. http:\/\/www.eclipse.org\/etrice\/\/.  2012-2017. etrice. http:\/\/www.eclipse.org\/etrice\/\/."},{"key":"e_1_3_2_1_13_1","unstructured":"2015. franca. https:\/\/github.com\/franca\/franca.  2015. franca. https:\/\/github.com\/franca\/franca."},{"key":"e_1_3_2_1_14_1","unstructured":"2018. BaSys. https:\/\/www.basys40.de.  2018. BaSys. https:\/\/www.basys40.de."},{"key":"e_1_3_2_1_15_1","unstructured":"2018. CBMD - Contract Based Modeling and Design Zentrales Innovationsprogramm Mittelstand (ZIM) (F\u00f6rderkennzeichen (FKZ): 16KN044132).  2018. CBMD - Contract Based Modeling and Design Zentrales Innovationsprogramm Mittelstand (ZIM) (F\u00f6rderkennzeichen (FKZ): 16KN044132)."},{"volume-title":"The B-book: assigning programs to meanings","author":"Abrial Jean-Raymond","key":"e_1_3_2_1_16_1","unstructured":"Jean-Raymond Abrial and Jean-Raymond Abrial . 2005. The B-book: assigning programs to meanings . Cambridge University Press . Jean-Raymond Abrial and Jean-Raymond Abrial. 2005. The B-book: assigning programs to meanings. Cambridge University Press."},{"key":"e_1_3_2_1_17_1","volume-title":"Tool Support for Live Formal Verification. In 20th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017","author":"Aravantinos Vincent","year":"2017","unstructured":"Vincent Aravantinos and Sudeep Kanav . 2017 . Tool Support for Live Formal Verification. In 20th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017 , Austin, TX, USA, September 17--22 , 2017. IEEE Computer Society, 145--155. Vincent Aravantinos and Sudeep Kanav. 2017. Tool Support for Live Formal Verification. In 20th ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS 2017, Austin, TX, USA, September 17--22, 2017. IEEE Computer Society, 145--155."},{"key":"e_1_3_2_1_18_1","unstructured":"Vincent Aravantinos Sebastian Voss Sabine Teufl Florian H\u00f6lzl and Bernhard Sch\u00e4tz. 2015. AutoFOCUS 3: Tooling Concepts for Seamless Model-based Development of Embedded Systems.. In ACES-MB&WUCOR@ MoDELS. 19--26.  Vincent Aravantinos Sebastian Voss Sabine Teufl Florian H\u00f6lzl and Bernhard Sch\u00e4tz. 2015. AutoFOCUS 3: Tooling Concepts for Seamless Model-based Development of Embedded Systems.. In ACES-MB&WUCOR@ MoDELS. 19--26."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604140"},{"key":"e_1_3_2_1_20_1","volume-title":"International Conference on Software Language Engineering. Springer, 296--305","author":"Barroca Bruno","year":"2010","unstructured":"Bruno Barroca , Levi L\u00facio , Vasco Amaral , Roberto F\u00e9lix , and Vasco Sousa . 2010 . Dsltrans: A turing incomplete transformation language . In International Conference on Software Language Engineering. Springer, 296--305 . Bruno Barroca, Levi L\u00facio, Vasco Amaral, Roberto F\u00e9lix, and Vasco Sousa. 2010. Dsltrans: A turing incomplete transformation language. In International Conference on Software Language Engineering. Springer, 296--305."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022905120346"},{"key":"e_1_3_2_1_22_1","unstructured":"Sam Blackshear and Dino Distefano. {n. d.}. Finding inter-procedural bugs at scale with Infer static analyzer. \"https:\/\/code.fb.com\/developer-tools\/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer\/\" Accessed: 2017-04-19.  Sam Blackshear and Dino Distefano. {n. d.}. Finding inter-procedural bugs at scale with Infer static analyzer. \"https:\/\/code.fb.com\/developer-tools\/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer\/\" Accessed: 2017-04-19."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2427376.2427379"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986345"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693137"},{"key":"e_1_3_2_1_26_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS","author":"Clarke Edmund M.","year":"2004","unstructured":"Edmund M. Clarke , Daniel Kroening , and Flavio Lerda . 2004. A Tool for Checking ANSI-C Programs . In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004 , Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings . 168--176. Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. 168--176."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2023522.2023528"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2022007.2022012"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2339852"},{"key":"e_1_3_2_1_30_1","first-page":"23","article-title":"Acceptance of formal methods: Lessons from hardware design","volume":"29","author":"Dill David L","year":"1996","unstructured":"David L Dill and John Rushby . 1996 . Acceptance of formal methods: Lessons from hardware design . IEEE Computer 29 , 4 (1996), 23 -- 24 . David L Dill and John Rushby. 1996. Acceptance of formal methods: Lessons from hardware design. IEEE Computer 29, 4 (1996), 23--24.","journal-title":"IEEE Computer"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"e_1_3_2_1_32_1","unstructured":"Sanford Friedenthal Alan Moore and Rick Steiner. 2014. A practical guide to SysML: the systems modeling language. Morgan Kaufmann.   Sanford Friedenthal Alan Moore and Rick Steiner. 2014. A practical guide to SysML: the systems modeling language. Morgan Kaufmann."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1815297.1815300"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220880.3220971"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486877"},{"volume-title":"Recommendations for implementing the strategic initiative INDUSTRIE 4.0: Securing the future of German manufacturing industry","author":"Kagermann Henning","key":"e_1_3_2_1_38_1","unstructured":"Henning Kagermann , Johannes Helbig , Ariane Hellinger , and Wolfgang Wahlster . 2013. Recommendations for implementing the strategic initiative INDUSTRIE 4.0: Securing the future of German manufacturing industry ; final report of the Industrie 4.0 Working Group . Forschungsunion. Henning Kagermann, Johannes Helbig, Ariane Hellinger, and Wolfgang Wahlster. 2013. Recommendations for implementing the strategic initiative INDUSTRIE 4.0: Securing the future of German manufacturing industry; final report of the Industrie 4.0 Working Group. Forschungsunion."},{"key":"e_1_3_2_1_39_1","volume-title":"Modular transformation from AF3 to nuXmv. MoDeVVa @ MoDELS","author":"Kanav Sudeep","year":"2017","unstructured":"Sudeep Kanav and Vincent Aravantinos . 2017. Modular transformation from AF3 to nuXmv. MoDeVVa @ MoDELS ( 2017 ). Sudeep Kanav and Vincent Aravantinos. 2017. Modular transformation from AF3 to nuXmv. MoDeVVa @ MoDELS (2017)."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ESEM.2007.82"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0429-x"},{"key":"e_1_3_2_1_42_1","volume-title":"Cl\u00e1udio Gomes, Gehan MK Selim, Juergen Dingel, James R Cordy, and Hans Vangheluwe.","author":"L\u00facio Levi","year":"2015","unstructured":"Levi L\u00facio , Bentley James Oakes , Cl\u00e1udio Gomes, Gehan MK Selim, Juergen Dingel, James R Cordy, and Hans Vangheluwe. 2015 . SyVOLT: Full Model Transformation Verification Using Contracts.. In P&D@ MoDELS. 24--27. Levi L\u00facio, Bentley James Oakes, Cl\u00e1udio Gomes, Gehan MK Selim, Juergen Dingel, James R Cordy, and Hans Vangheluwe. 2015. SyVOLT: Full Model Transformation Verification Using Contracts.. In P&D@ MoDELS. 24--27."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_31"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"},{"key":"e_1_3_2_1_46_1","unstructured":"Rutger van Beusekom Jan Friso Groote Rob Howe Wieger Wesselink Rob Wieringa and Tim AC Willemse. {n. d.}. From Dezyne to Model Checking. ({n. d.}).  Rutger van Beusekom Jan Friso Groote Rob Howe Wieger Wesselink Rob Wieringa and Tim AC Willemse. {n. d.}. From Dezyne to Model Checking. ({n. d.})."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384716.2384767"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2016.2521368"}],"event":{"name":"MODELS '18: ACM\/IEEE 21th International Conference on Model Driven Engineering Languages and Systems","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Copenhagen Denmark","acronym":"MODELS '18"},"container-title":["Proceedings of the 21st ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3270112.3275334","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3270112.3275334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:26Z","timestamp":1750208546000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3270112.3275334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,14]]},"references-count":47,"alternative-id":["10.1145\/3270112.3275334","10.1145\/3270112"],"URL":"https:\/\/doi.org\/10.1145\/3270112.3275334","relation":{},"subject":[],"published":{"date-parts":[[2018,10,14]]},"assertion":[{"value":"2018-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}