{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,1]],"date-time":"2024-04-01T11:49:29Z","timestamp":1711972169789},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T00:00:00Z","timestamp":1550448000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1007\/s10009-019-00510-w","type":"journal-article","created":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T17:07:40Z","timestamp":1550509660000},"page":"267-286","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["An integrated environment for Spin-based C code checking"],"prefix":"10.1007","volume":"21","author":[{"given":"Daniel","family":"Ratiu","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Ulrich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,2,18]]},"reference":[{"issue":"2","key":"510_CR1","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1109\/TSE.2011.121","volume":"38","author":"A Arcuri","year":"2012","unstructured":"Arcuri, A., Iqbal, M.Z., Briand, L.: Random testing: theoretical results and practical implications. IEEE Trans. Softw. Eng. 38(2), 258\u2013277 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"510_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses report on SV-COMP 2016. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"510_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Computer Aided Verification (CAV). Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"510_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Lemberger, T.: Software verification: testing vs. model checking. In: Hardware and Software: Verification and Testing. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-70389-3_7"},{"key":"510_CR5","doi-asserted-by":"crossref","unstructured":"Brezocnik, Z., Vlaovic, B., Vreze, A.: SpinRCP: the Eclipse rich client platform integrated development environment for the Spin model checker. In: International Symposium on Model Checking of Software (2014)","DOI":"10.1145\/2632362.2632380"},{"key":"510_CR6","volume-title":"The MPS Language Workbench","author":"F Campagne","year":"2014","unstructured":"Campagne, F.: The MPS Language Workbench. CreateSpace Publishing, Scotts Valley (2014)"},{"key":"510_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"510_CR8","doi-asserted-by":"crossref","unstructured":"Donaldson, A.F., Gay, S.J.: ETCH: An enhanced type checking tool for Promela. In: Workshop on Model Checking Software (SPIN). Springer (2005)","DOI":"10.1007\/11537328_21"},{"key":"510_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/bs.adcom.2015.11.003","volume":"101","author":"M Felderer","year":"2016","unstructured":"Felderer, M., B\u00fcchler, M., Johns, M., Brucker, A.D., Breu, R., Pretschner, A.: Security testing: a survey. Adv. Comput. 101, 1\u201351 (2016)","journal-title":"Adv. Comput."},{"issue":"1","key":"510_CR10","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1109\/TC.1982.1675885","volume":"31","author":"H Garcia-Molina","year":"1982","unstructured":"Garcia-Molina, H.: Elections in a distributed computing system. IEEE Trans. Comput. 31(1), 48\u201359 (1982)","journal-title":"IEEE Trans. Comput."},{"key":"510_CR11","doi-asserted-by":"crossref","unstructured":"Groce, A., Joshi, R.: Random testing and model checking: Building a common framework for nondeterministic exploration. In: International Workshop on Dynamic Analysis (WODA) (2008)","DOI":"10.1145\/1401827.1401833"},{"key":"510_CR12","doi-asserted-by":"crossref","unstructured":"Groce, A., Pinto, J.: A little language for testing. In: NASA Formal Methods (NFM) (2015)","DOI":"10.1007\/978-3-319-17524-9_15"},{"issue":"1","key":"510_CR13","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10009-016-0445-y","volume":"20","author":"J Holmes","year":"2018","unstructured":"Holmes, J., Groce, A., Pinto, J., Mittal, P., Azimi, P., Kellar, K., O\u2019Brien, J.: TSTL: the template scripting testing language. STTT 20(1), 57\u201378 (2018)","journal-title":"STTT"},{"key":"510_CR14","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley, Boston (2011)","edition":"1"},{"key":"510_CR15","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10515-008-0033-9","volume":"15","author":"G Holzmann","year":"2008","unstructured":"Holzmann, G., Joshi, R., Groce, A.: Model driven code checking. Autom. Softw. Eng. 15, 283\u2013297 (2008)","journal-title":"Autom. Softw. Eng."},{"key":"510_CR16","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Workshop on Model Checking Software (SPIN) (2004)","DOI":"10.1007\/978-3-540-24732-6_6"},{"key":"510_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/bs.adcom.2015.05.003","volume":"99","author":"DR Kuhn","year":"2015","unstructured":"Kuhn, D.R., Bryce, R., Duan, F., Ghandehari, L.S., Lei, Y., Kacker, R.N.: Combinatorial testing: theory and practice. Adv. Comput. 99, 1\u201366 (2015)","journal-title":"Adv. Comput."},{"key":"510_CR18","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis and transformation. In: International Symposium on Code Generation and Optimization (2004)"},{"key":"510_CR19","doi-asserted-by":"crossref","unstructured":"Mali, Y., Wyk, E.V.: Building extensible specifications and implementations of Promela with AbleP. In: Workshop on Model Checking Software (SPIN) (2011)","DOI":"10.1007\/978-3-642-22306-8_8"},{"key":"510_CR20","unstructured":"European Union Agency for Railways: ERTMS\/ETCS Baseline 3: System Requirements Specifications. SUBSET-026 (2014). Issue 3.4.0"},{"key":"510_CR21","unstructured":"Synopsys, Inc.: Static application security testing (coverity). \n                    https:\/\/www.synopsys.com\/software-integrity\/security-testing\/static-analysis-sast.html\n                    \n                   (2018). Accessed 9 Apr 2018"},{"key":"510_CR22","unstructured":"The Clang Team: Clang Compiler User\u2019s Manual (2018). \n                    https:\/\/clang.llvm.org\/docs\/UsersManual.html\n                    \n                  . Accessed 9 Apr 2018"},{"key":"510_CR23","unstructured":"The MathWorks, Inc.: Polyspace \u2013 making critical code safe and secure. \n                    https:\/\/de.mathworks.com\/products\/polyspace.html\n                    \n                   (2018). Accessed 9 Apr 2018"},{"key":"510_CR24","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1002\/stvr.294","volume":"14","author":"P McMinn","year":"2004","unstructured":"McMinn, P.: Search-based software test data generation: a survey. Softw. Test. Verif. Reliab. 14, 105\u2013156 (2004)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"510_CR25","doi-asserted-by":"crossref","unstructured":"Molotnikov, Z., V\u00f6lter, M., Ratiu, D.: Automated domain-specific C verification with mbeddr. In: International Conference on Automatic Software Engineering (ASE) (2014)","DOI":"10.1145\/2642937.2642938"},{"key":"510_CR26","unstructured":"Pierre\u00a0Meyer Richard\u00a0Chavagnat, F.B.: Computation of the safe emergency braking deceleration for trains operated by ETCS\/ERTMS using the monte carlo statistical approach. In: Proceedings of the 9th World Congress of Railway Research (WCRR) (2011)"},{"key":"510_CR27","doi-asserted-by":"crossref","unstructured":"Ratiu, D., Ulrich, A.: Increasing usability of Spin-based C code verification using a harness definition language. In: International SPIN Symposium on Model Checking of Software, SPIN 2017 (2017)","DOI":"10.1145\/3092282.3092283"},{"key":"510_CR28","doi-asserted-by":"crossref","unstructured":"Ratiu, D., Voelter, M., Kolb, B., Sch\u00e4tz, B.: Using language engineering to lift languages and analyses at the domain level. In: NASA Formal Methods Symposium (NFM) (2013)","DOI":"10.1007\/978-3-642-38088-4_35"},{"key":"510_CR29","doi-asserted-by":"crossref","unstructured":"Ruys, T.C.: Low-fat recipes for SPIN. In: International Workshop on SPIN Model Checking and Software Verification. Springer (2000)","DOI":"10.1007\/10722468_17"},{"key":"510_CR30","unstructured":"Serebryany, K., Bruening, D., Potapenko, A., Vyukov, D.: Addresssanitizer: A fast address sanity checker. In: Proceedings of the 2012 USENIX Conference on Annual Technical Conference. USENIX Association (2012)"},{"key":"510_CR31","doi-asserted-by":"crossref","unstructured":"Stepanov, E., Serebryany, K.: Memorysanitizer: fast detector of uninitialized memory use in c++. In: International Symposium on Code Generation and Optimization, CGO \u201915. Washington, DC, USA (2015)","DOI":"10.1109\/CGO.2015.7054186"},{"key":"510_CR32","unstructured":"Stephan Horn, O.P.: Chancen und m\u00f6glichkeiten der monte-carlo-methode bei der bestimmung der etcs-bremskurven. In: Eisenbahntechnische Rundschau (ETR) (2017)"},{"key":"510_CR33","doi-asserted-by":"crossref","unstructured":"Sulzmann, M., Zechner, A.: Model checking dsl-generated C source code. In: International Workshop on Model Checking Software (SPIN) (2012)","DOI":"10.1007\/978-3-642-31759-0_18"},{"key":"510_CR34","unstructured":"Voelter, M., Benz, S., Dietrich, C., Engelmann, B., Helander, M., Kats, L., Visser, E., Wachsmuth, G.: DSL Engineering. \n                    http:\/\/dslbook.org\n                    \n                   (2013)"},{"key":"510_CR35","doi-asserted-by":"crossref","unstructured":"Voelter, M., Kolb, B., Szab\u00f3, T., Ratiu, D., van Deursen, A.: Lessons learned from developing mbeddr: a case study in language engineering with mps. Softw. Syst. Model. pp. 1\u201346 (2017)","DOI":"10.1007\/s10270-016-0575-4"},{"key":"510_CR36","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/s10515-013-0120-4","volume":"20","author":"M Voelter","year":"2013","unstructured":"Voelter, M., Ratiu, D., Kolb, B., Sch\u00e4tz, B.: mbeddr: instantiating a language workbench in the embedded software domain. Autom. Softw. Eng. 20, 339\u2013390 (2013)","journal-title":"Autom. Softw. Eng."},{"key":"510_CR37","doi-asserted-by":"crossref","unstructured":"de Vos, B., Kats, L.C.L., Pronk, C.: EpiSpin: an eclipse plug-in for promela\/spin using spoofax. In: International Workshop on Model Checking Software (SPIN) (2011)","DOI":"10.1007\/978-3-642-22306-8_12"},{"key":"510_CR38","doi-asserted-by":"crossref","unstructured":"Yatake, K., Aoki, T.: Automatic generation of model checking scripts based on environment modeling. In: International Conference on Model Checking Software (SPIN). Springer (2010)","DOI":"10.1007\/978-3-642-16164-3_5"},{"key":"510_CR39","doi-asserted-by":"crossref","unstructured":"Yu, L., Lei, Y., Kacker, R.N., Kuhn, D.R.: Acts: a combinatorial test generation tool. In: International Conference on Software Testing, Verification and Validation (2013)","DOI":"10.1109\/ICST.2013.52"},{"key":"510_CR40","unstructured":"Zalewski, M.: American fuzzy lop. \n                    http:\/\/lcamtuf.coredump.cx\/afl\/\n                    \n                   (2018). Accessed 29 Apr 2018"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00510-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00510-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00510-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,18]],"date-time":"2020-02-18T16:14:05Z","timestamp":1582042445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00510-w"}},"subtitle":["Towards bringing model-driven code checking closer to practitioners"],"short-title":[],"issued":{"date-parts":[[2019,2,18]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,6]]}},"alternative-id":["510"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00510-w","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2,18]]},"assertion":[{"value":"18 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}