{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T15:05:12Z","timestamp":1761491112202,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,16]],"date-time":"2020-10-16T00:00:00Z","timestamp":1602806400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Marie Sk?odowska-Curie Actions","award":["813884"],"award-info":[{"award-number":["813884"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,16]]},"DOI":"10.1145\/3417990.3421407","type":"proceedings-article","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T14:03:12Z","timestamp":1604325792000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Model checking as a service"],"prefix":"10.1145","author":[{"given":"Benedek","family":"Horv\u00e1th","sequence":"first","affiliation":[{"name":"Johannes Kepler University Linz, Linz, Austria"}]},{"given":"Bence","family":"Graics","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"\u00c1kos","family":"Hajdu","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"Zolt\u00e1n","family":"Micskei","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"Vince","family":"Moln\u00e1r","sequence":"additional","affiliation":[{"name":"Budapest University of Technology and Economics, Budapest, Hungary"}]},{"given":"Istv\u00e1n","family":"R\u00e1th","sequence":"additional","affiliation":[{"name":"IncQuery Labs Ltd., Budapest, Hungary"}]},{"given":"Luigi","family":"Andolfato","sequence":"additional","affiliation":[{"name":"European Southern Observatory, M\u00fcnchen, Germany"}]},{"given":"Ivan","family":"Gomes","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}]},{"given":"Robert","family":"Karban","sequence":"additional","affiliation":[{"name":"California Institute of Technology"}]}],"member":"320","published-online":{"date-parts":[[2020,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21732-6_12"},{"volume-title":"Handbook of model checking","author":"Clarke Edmund M","key":"e_1_3_2_1_4_1","unstructured":"Edmund M Clarke , Thomas A Henzinger , Helmut Veith , and Roderick P Bloem . 2018. Handbook of model checking . Springer . Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick P Bloem. 2018. Handbook of model checking. Springer."},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems. JACoW, 911--914","author":"Darvas D\u00e1niel","year":"2015","unstructured":"D\u00e1niel Darvas , Borja Fern\u00e1ndez Adiego , and Enrique Blanco Vi\u00f1uela . 2015 . PLCverif: A tool to verify PLC programs based on model checking techniques . In Proc. of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems. JACoW, 911--914 . D\u00e1niel Darvas, Borja Fern\u00e1ndez Adiego, and Enrique Blanco Vi\u00f1uela. 2015. PLCverif: A tool to verify PLC programs based on model checking techniques. In Proc. of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems. JACoW, 911--914."},{"key":"e_1_3_2_1_6_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. LNCS","volume":"8413","author":"Robinson Thomas","unstructured":"Thomas G.- Robinson , Philip J. Armstrong , Alexandre Boulgakov , and A. W. Roscoe . 2014. FDR3 - A Modern Refinement Checker for CSP . In Tools and Algorithms for the Construction and Analysis of Systems. LNCS , Vol. 8413 . Springer, 187--201. Thomas G.-Robinson, Philip J. Armstrong, Alexandre Boulgakov, and A. W. Roscoe. 2014. FDR3 - A Modern Refinement Checker for CSP. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS, Vol. 8413. Springer, 187--201."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2557833.2560583"},{"key":"e_1_3_2_1_8_1","volume-title":"Day","author":"Gibson Corrina","year":"2014","unstructured":"Corrina Gibson , Robert Karban , Luigi Andolfato , and John C . Day . 2014 . Abstractions for Executable and Checkable Fault Management Models. In Proc. of the Conference on Systems Engineering Research. Elsevier , 146--154. Corrina Gibson, Robert Karban, Luigi Andolfato, and John C. Day. 2014. Abstractions for Executable and Checkable Fault Management Models. In Proc. of the Conference on Systems Engineering Research. Elsevier, 146--154."},{"volume-title":"Model-Driven Design and Verification of Component-Based Reactive Systems. Bachelor's thesis","author":"Graics Bence","key":"e_1_3_2_1_9_1","unstructured":"Bence Graics . 2016. Model-Driven Design and Verification of Component-Based Reactive Systems. Bachelor's thesis . Budapest University of Technology and Economics . Bence Graics. 2016. Model-Driven Design and Verification of Component-Based Reactive Systems. Bachelor's thesis. Budapest University of Technology and Economics."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3270112.3270125"},{"volume-title":"Modeling, Systems Engineering, and Project Management for Astronomy VII","author":"Karban Robert","key":"e_1_3_2_1_11_1","unstructured":"Robert Karban , Frank G. Dekens , Sebastian Herzig , Maged Elaasar , and Nerijus Jankevi\u010dius . 2016. Creating system engineering products with executable models in a model-based engineering environment . In Modeling, Systems Engineering, and Project Management for Astronomy VII , Vol. 9911 . SPIE , 96--111. Robert Karban, Frank G. Dekens, Sebastian Herzig, Maged Elaasar, and Nerijus Jankevi\u010dius. 2016. Creating system engineering products with executable models in a model-based engineering environment. In Modeling, Systems Engineering, and Project Management for Astronomy VII, Vol. 9911. SPIE, 96--111."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001659970003"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10181-1_9"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11245-9_1"},{"key":"e_1_3_2_1_15_1","volume-title":"Proc. of the 1st Workshop on Open Source Software for Model Driven Engineering","volume":"1290","author":"Micskei Zolt\u00e1n","year":"2014","unstructured":"Zolt\u00e1n Micskei , Raimund-Andreas Konnerth , Benedek Horv\u00e1th , Oszk\u00e1r Semerath , Andr\u00e1s V\u00f6r\u00f6s , and D\u00e1niel Varr\u00f3 . 2014 . On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf . In Proc. of the 1st Workshop on Open Source Software for Model Driven Engineering , Vol. 1290 . CEUR, 31--41. Zolt\u00e1n Micskei, Raimund-Andreas Konnerth, Benedek Horv\u00e1th, Oszk\u00e1r Semerath, Andr\u00e1s V\u00f6r\u00f6s, and D\u00e1niel Varr\u00f3. 2014. On Open Source Tools for Behavioral Modeling and Analysis with fUML and Alf. In Proc. of the 1st Workshop on Open Source Software for Model Driven Engineering, Vol. 1290. CEUR, 31--41."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-018-00710-z"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183489"},{"key":"e_1_3_2_1_18_1","unstructured":"OMG. 2017. Action Language for Foundational UML (Alf). formal\/17-07-04.  OMG. 2017. Action Language for Foundational UML (Alf). formal\/17-07-04."},{"key":"e_1_3_2_1_19_1","unstructured":"OMG. 2018. Semantics of a Foundational Subset for Executable UML Models (fUML). formal\/18-12-01.  OMG. 2018. Semantics of a Foundational Subset for Executable UML Models (fUML). formal\/18-12-01."},{"key":"e_1_3_2_1_20_1","unstructured":"OMG. 2019. OMG System Modeling Language (SysML). formal\/19-11-01.  OMG. 2019. OMG System Modeling Language (SysML). formal\/19-11-01."},{"key":"e_1_3_2_1_21_1","unstructured":"OMG. 2019. Precise Semantics of UML State Machines (PSSM). formal\/19-05-01.  OMG. 2019. Precise Semantics of UML State Machines (PSSM). formal\/19-05-01."},{"key":"e_1_3_2_1_22_1","volume-title":"Software Engineering for Self-Adaptive Systems III (LNCS","volume":"153","author":"Sharifloo Amir Molzam","year":"2013","unstructured":"Amir Molzam Sharifloo and Andreas Metzger . 2013 . MCaaS: Model Checking in the Cloud for Assurances of Adaptive Systems . In Software Engineering for Self-Adaptive Systems III (LNCS , Vol. 9640). Springer, 137-- 153 . Amir Molzam Sharifloo and Andreas Metzger. 2013. MCaaS: Model Checking in the Cloud for Assurances of Adaptive Systems. In Software Engineering for Self-Adaptive Systems III (LNCS, Vol. 9640). Springer, 137--153."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-012-0281-9"},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. of the 13th Workshop on Model-Driven Engineering, Verification and Validation","volume":"1713","author":"Zalila Faiez","year":"2016","unstructured":"Faiez Zalila , Xavier Cr\u00e9gut , and Marc Pantel . 2016 . A DSL to Feedback Formal Verification Results . In Proc. of the 13th Workshop on Model-Driven Engineering, Verification and Validation , Vol. 1713 . CEUR, 30--39. Faiez Zalila, Xavier Cr\u00e9gut, and Marc Pantel. 2016. A DSL to Feedback Formal Verification Results. In Proc. of the 13th Workshop on Model-Driven Engineering, Verification and Validation, Vol. 1713. CEUR, 30--39."}],"event":{"name":"MODELS '20: ACM\/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Virtual Event Canada","acronym":"MODELS '20"},"container-title":["Proceedings of the 23rd ACM\/IEEE International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417990.3421407","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3417990.3421407","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:35Z","timestamp":1750195895000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3417990.3421407"}},"subtitle":["towards pragmatic hidden formal methods"],"short-title":[],"issued":{"date-parts":[[2020,10,16]]},"references-count":25,"alternative-id":["10.1145\/3417990.3421407","10.1145\/3417990"],"URL":"https:\/\/doi.org\/10.1145\/3417990.3421407","relation":{},"subject":[],"published":{"date-parts":[[2020,10,16]]},"assertion":[{"value":"2020-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}