{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,18]],"date-time":"2026-07-18T16:31:42Z","timestamp":1784392302014,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T00:00:00Z","timestamp":1565568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council under the European Union?s Horizon 2020 research and innovation programme","award":["694277"],"award-info":[{"award-number":["694277"]}]},{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["BRIDGES18\/IS\/12632261"],"award-info":[{"award-number":["BRIDGES18\/IS\/12632261"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Horizon 2020","award":["694277"],"award-info":[{"award-number":["694277"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,12]]},"DOI":"10.1145\/3338906.3340444","type":"proceedings-article","created":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T12:21:03Z","timestamp":1565353263000},"page":"1015-1025","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Evaluating model testing and model checking for finding requirements violations in Simulink models"],"prefix":"10.1145","author":[{"given":"Shiva","family":"Nejati","sequence":"first","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Khouloud","family":"Gaaloul","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Claudio","family":"Menghi","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lionel C.","family":"Briand","sequence":"additional","affiliation":[{"name":"University of Luxembourg, Luxembourg"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Foster","sequence":"additional","affiliation":[{"name":"QRA, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Wolfe","sequence":"additional","affiliation":[{"name":"QRA, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,8,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"d.}. Mathematica. https:\/\/www.wolfram.com\/mathematica\/. ({n. d.}). Accessed: 2019-04-26","year":"2019","unstructured":"{n. d.}. Mathematica. https:\/\/www.wolfram.com\/mathematica\/. ({n. d.}). Accessed: 2019-04-26 . 2019 . Companion material. https:\/\/www.dropbox.com\/sh\/i9n764r1q6vjkxz\/ AADsgN-gvX-ystJPMDVVjYhga ?dl=0. (26 04 2019). 2019. qracorp. (2019). https:\/\/qracorp.com 2019. QVtrace. https:\/\/qracorp.com\/qvtrace\/. (01 02 2019). {n. d.}. Mathematica. https:\/\/www.wolfram.com\/mathematica\/. ({n. d.}). Accessed: 2019-04-26. 2019. Companion material. https:\/\/www.dropbox.com\/sh\/i9n764r1q6vjkxz\/ AADsgN-gvX-ystJPMDVVjYhga?dl=0. (26 04 2019). 2019. qracorp. (2019). https:\/\/qracorp.com 2019. QVtrace. https:\/\/qracorp.com\/qvtrace\/. (01 02 2019)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465787.2465797"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970311"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"e_1_3_2_1_5_1","volume-title":"Principles of Cyber-Physical Systems","author":"Alur Rajeev","unstructured":"Rajeev Alur . 2015. Principles of Cyber-Physical Systems . MIT Press . Rajeev Alur. 2015. Principles of Cyber-Physical Systems. MIT Press."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-016-0207-9"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2012.42"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889212"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050917.2050919"},{"key":"e_1_3_2_1_12_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Jr., Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press , Cambridge, MA, USA. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA, USA."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70930-5_6"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_15_1","volume-title":"SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. 351\u2013368","author":"Donaldson Alastair F.","year":"2011","unstructured":"Alastair F. Donaldson , Leopold Haller , Daniel Kroening , and Philipp R\u00fcmmer . 2011 . Software Verification Using k-Induction. In Static Analysis - 18th International Symposium , SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. 351\u2013368 . Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp R\u00fcmmer. 2011. Software Verification Using k-Induction. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings. 351\u2013368."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2016.16"},{"key":"e_1_3_2_1_18_1","volume-title":"AFM","author":"Hamon Gregoire","year":"2008","unstructured":"Gregoire Hamon . 2008 . Simulink Design Verifier - Applying Automated Formal Methods to Simulink and Stateflow . In AFM 2008. Citeseer. Gregoire Hamon. 2008. Simulink Design Verifier - Applying Automated Formal Methods to Simulink and Stateflow. In AFM 2008. Citeseer."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_2_1_20_1","volume-title":"Kochenderfer","author":"Katz Guy","year":"2017","unstructured":"Guy Katz , Clark W. Barrett , David L. Dill , Kyle Julian , and Mykel J . Kochenderfer . 2017 . Reluplex : An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs\/1702.01135 (2017). http:\/\/arxiv.org\/abs\/1702.01135 Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CoRR abs\/1702.01135 (2017). http:\/\/arxiv.org\/abs\/1702.01135"},{"key":"e_1_3_2_1_21_1","volume-title":"Logic in Computer Science","author":"Larsen Kim G","unstructured":"Kim G Larsen and Bent Thomsen . 1988. A modal process logic . In Logic in Computer Science . IEEE , 203\u2013210. Kim G Larsen and Bent Thomsen. 1988. A modal process logic. In Logic in Computer Science. IEEE, 203\u2013210."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939399.1939412"},{"key":"e_1_3_2_1_23_1","volume-title":"Essentials of Metaheuristics","author":"Luke Sean","unstructured":"Sean Luke . 2013. Essentials of Metaheuristics ( second ed.). Lulu . Sean Luke. 2013. Essentials of Metaheuristics (second ed.). Lulu."},{"key":"e_1_3_2_1_24_1","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","unstructured":"Oded Maler and Dejan Nickovic . 2004. Monitoring temporal properties of continuous signals . In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems . Springer , 152\u2013166. Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152\u2013166."},{"key":"e_1_3_2_1_25_1","volume-title":"Test Generation and Test Prioritization for Simulink Models with Dynamic Behavior","author":"Matinnejad Reza","year":"2018","unstructured":"Reza Matinnejad , Shiva Nejati , Lionel Briand , and Thomas Bruckmann . 2018. Test Generation and Test Prioritization for Simulink Models with Dynamic Behavior . IEEE Transactions on Software Engineering ( 2018 ). Reza Matinnejad, Shiva Nejati, Lionel Briand, and Thomas Bruckmann. 2018. Test Generation and Test Prioritization for Simulink Models with Dynamic Behavior. IEEE Transactions on Software Engineering (2018)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3117770"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642978"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884797"},{"key":"e_1_3_2_1_29_1","volume-title":"Search-based automated testing of continuous controllers: Framework, tool support, and case studies. Information &amp","author":"Matinnejad Reza","year":"2015","unstructured":"Reza Matinnejad , Shiva Nejati , Lionel C. Briand , Thomas Bruckmann , and Claude Poull . 2015. Search-based automated testing of continuous controllers: Framework, tool support, and case studies. Information &amp ; Software Technology 57 ( 2015 ), 705\u2013722. Reza Matinnejad, Shiva Nejati, Lionel C. Briand, Thomas Bruckmann, and Claude Poull. 2015. Search-based automated testing of continuous controllers: Framework, tool support, and case studies. Information & Software Technology 57 (2015), 705\u2013722."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1077276.1077279"},{"key":"e_1_3_2_1_31_1","volume-title":"Briand","author":"Menghi Claudio","year":"2019","unstructured":"Claudio Menghi , Shiva Nejati , Khouloud Gaaloul , and Lionel C . Briand . 2019 . Generating Automated and Online Test Oracles for Simulink Models with Continuous and Uncertain Behaviors. CoRR abs\/1903.03399 (2019). arXiv: 1903.03399 http:\/\/arxiv.org\/abs\/1903.03399 Claudio Menghi, Shiva Nejati, Khouloud Gaaloul, and Lionel C. Briand. 2019. Generating Automated and Online Test Oracles for Simulink Models with Continuous and Uncertain Behaviors. CoRR abs\/1903.03399 (2019). arXiv: 1903.03399 http:\/\/arxiv.org\/abs\/1903.03399"},{"key":"e_1_3_2_1_32_1","volume-title":"Control Systems Engineering","author":"Nise N. S.","unstructured":"N. S. Nise . 2004. Control Systems Engineering ( 4 th ed.). John-Wiely Sons . N. S. Nise. 2004. Control Systems Engineering (4th ed.). John-Wiely Sons.","edition":"4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_1_34_1","unstructured":"Prover Technology. {n. d.}. Prover Plug-In Software. http:\/\/www.prover.com. ({n. d.}). {Online; accessed 17-Aug-2015}.  Prover Technology. {n. d.}. Prover Plug-In Software. http:\/\/www.prover.com. ({n. d.}). {Online; accessed 17-Aug-2015}."},{"key":"e_1_3_2_1_35_1","volume-title":"http:\/\/www.reactive-systems.com\/simulinktesting-validation.html. (2010). {Online","author":"Reactive Systems Inc. 2010. Reactis Tester.","year":"2015","unstructured":"Reactive Systems Inc. 2010. Reactis Tester. http:\/\/www.reactive-systems.com\/simulinktesting-validation.html. (2010). {Online ; accessed 17- Aug- 2015 }. Reactive Systems Inc. 2010. Reactis Tester. http:\/\/www.reactive-systems.com\/simulinktesting-validation.html. (2010). {Online; accessed 17-Aug-2015}."},{"key":"e_1_3_2_1_36_1","unstructured":"The MathWorks Inc. {n. d.}. Simulink Design Verifier. http:\/\/nl.mathworks.com\/ products\/sldesignverifier\/?refresh=true. ({n. d.}). {Online; accessed 17-Aug-2015}.  The MathWorks Inc. {n. d.}. Simulink Design Verifier. http:\/\/nl.mathworks.com\/ products\/sldesignverifier\/?refresh=true. ({n. d.}). {Online; accessed 17-Aug-2015}."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.05.002"},{"key":"e_1_3_2_1_38_1","volume-title":"Model-based testing for embedded systems","author":"Zander Justyna","unstructured":"Justyna Zander , Ina Schieferdecker , and Pieter J Mosterman . 2012. Model-based testing for embedded systems . CRC Press . Justyna Zander, Ina Schieferdecker, and Pieter J Mosterman. 2012. Model-based testing for embedded systems. CRC Press."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSYST.2015.2496293"}],"event":{"name":"ESEC\/FSE '19: 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Tallinn Estonia","acronym":"ESEC\/FSE '19","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338906.3340444","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3338906.3340444","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:21Z","timestamp":1750206381000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338906.3340444"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,12]]},"references-count":39,"alternative-id":["10.1145\/3338906.3340444","10.1145\/3338906"],"URL":"https:\/\/doi.org\/10.1145\/3338906.3340444","relation":{},"subject":[],"published":{"date-parts":[[2019,8,12]]},"assertion":[{"value":"2019-08-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}