{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T10:23:49Z","timestamp":1748600629533,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994280"},{"type":"electronic","value":"9783030994297"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Software doping is a phenomenon that refers to the presence of hidden software functionality, whose existence is only in the interest of the manufacturer. The most prominent example is the diesel emissions scandal. There is a need for methods that identify software doping, and such methods are bound to be applied to the final product with no or rare knowledge about its internals. Black-box analysis techniques have recently been developed for this purpose, harvesting the formal foundations of software doping. This paper integrates them with established falsification techniques for the purpose of real-world applicability. With a focus on the diesel scandal and emissions tests on chassis dynamometers we make the testing procedures significantly more effective in terms of time and cost. The theoretical results are implemented in a prototypical doping tester.<\/jats:p>","DOI":"10.1007\/978-3-030-99429-7_4","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"71-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On the Detection of Doped Software by Falsification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6897-2506","authenticated-orcid":false,"given":"Sebastian","family":"Biewer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Abbas, H., Fainekos, G.E., Sankaranarayanan, S., Ivancic, F., Gupta, A.: Probabilistic temporal logic falsification of cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(2s), 95:1\u201395:30 (2013). https:\/\/doi.org\/10.1145\/2465787.2465797","DOI":"10.1145\/2465787.2465797"},{"key":"4_CR2","unstructured":"Adroit, A.: Software-defined everything (SDE) market perspective (2021\u20132027): Cisco Systems Inc, Dell Inc, EMC Corp, Extreme Networks, Fujitsu Ltd, Hewlett Packard Enterprise. New Mexico Tribune (2021), https:\/\/nmtribune.com\/uncategorized\/199383\/software-defined-everything-sde-market-perspective-2021-2027-cisco-systems-inc-dell-inc-emc-corp-extreme-networks-fujitsu-ltd-hewlett-packard-enterprise\/, Online; accessed: 2021-07-13"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. In: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS \u201990), Philadelphia, Pennsylvania, USA, June 4-7, 1990. pp. 390\u2013401. IEEE Computer Society (1990). https:\/\/doi.org\/10.1109\/LICS.1990.113764","DOI":"10.1109\/LICS.1990.113764"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Mathematical Structures in Computer Science 21(6), 1207\u20131252 (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","DOI":"10.1017\/S0960129511000193"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Biewer, S., D\u2019Argenio, P., Hermanns, H.: Doping tests for cyber-physical systems. In: Parker, D., Wolf, V. (eds.) Quantitative Evaluation of Systems, 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11785, pp. 313\u2013331. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_18","DOI":"10.1007\/978-3-030-30281-8_18"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Biewer, S., D\u2019Argenio, P.R., Hermanns, H.: Doping tests for cyber-physical systems. ACM Trans. Model. Comput. Simul. 31(3), 16:1\u201316:27 (2021). https:\/\/doi.org\/10.1145\/3449354","DOI":"10.1145\/3449354"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Biewer, S., Dimitrova, R., Fries, M., Gazda, M., Heinze, T., Hermanns, H., Mousavi, M.R.: Conformance Relations and Hyperproperties for Doping Detection in Time and Space. Logical Methods in Computer Science 18(1), 14:1\u201314:39 (2022). https:\/\/doi.org\/10.46298\/lmcs-18(1:14)2022","DOI":"10.46298\/lmcs-18(1:14)2022"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Biewer, S., Finkbeiner, B., Hermanns, H., K\u00f6hl, M.A., Schnitzer, Y., Schwenger, M.: RTLola on board: Testing real driving emissions on your phone. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12652, pp. 365\u2013372. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_20","DOI":"10.1007\/978-3-030-72013-1_20"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Brim, L., Dluhos, P., Safranek, D., Vejpustek, T.: STL*: Extending signal temporal logic with signal-value freezing operator. Inf. Comput. 236, 52\u201367 (2014). https:\/\/doi.org\/10.1016\/j.ic.2014.01.012","DOI":"10.1016\/j.ic.2014.01.012"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Chib, S., Greenberg, E.: Understanding the metropolis-hastings algorithm. The american statistician 49(4), 327\u2013335 (1995). https:\/\/doi.org\/10.1080\/00031305.1995.10476177","DOI":"10.1080\/00031305.1995.10476177"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol.\u00a08414, pp. 265\u2013284. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Barthe, G., Biewer, S., Finkbeiner, B., Hermanns, H.: Is your software on dope? - Formal analysis of surreptitiously \u201cenhanced\u201d programs. In: Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Proceedings. LNCS, vol. 10201, pp. 83\u2013110. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4","DOI":"10.1007\/978-3-662-54434-1_4"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08044, pp. 264\u2013279. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19","DOI":"10.1007\/978-3-642-39799-8_19"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: Kroening, D., Pasareanu, C.S. (eds.) CAV 2015. LNCS, vol.\u00a09206, pp. 30\u201348. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"K\u00f6hl, M.A., Hermanns, H., Biewer, S.: Efficient monitoring of real driving emissions. In: Colombo, C., Leucker, M. (eds.) Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11237, pp. 299\u2013315. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_17","DOI":"10.1007\/978-3-030-03769-7_17"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol.\u00a03253, pp. 152\u2013166. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"4_CR18","unstructured":"Mathews, M.: Are You Ready for Software-Defined Everything? Wired, https:\/\/www.wired.com\/insights\/2013\/05\/are-you-ready-for-software-defined-everything\/, Online; accessed: 2021-07-13"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) Tests and Proofs - 5th International Conference, TAP@TOOLS 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06706, pp. 134\u2013151. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21768-5_11","DOI":"10.1007\/978-3-642-21768-5_11"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010. pp. 211\u2013220. ACM (2010). https:\/\/doi.org\/10.1145\/1755952.1755983","DOI":"10.1145\/1755952.1755983"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"Nguyen, L.V., Kapinski, J., Jin, X., Deshmukh, J.V., Johnson, T.T.: Hyperproperties of real-valued signals. In: Talpin, J., Derler, P., Schneider, K. (eds.) Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29 - October 02, 2017. pp. 104\u2013113. ACM (2017). https:\/\/doi.org\/10.1145\/3127041.3127058","DOI":"10.1145\/3127041.3127058"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR23","unstructured":"Rosen, K.H., Krithivasan, K.: Discrete mathematics and its applications: with combinatorics and graph theory. Tata McGraw-Hill Education (2012)"},{"key":"4_CR24","unstructured":"The European Parliament and the Council of the European Union: Commission Regulation (EU) 2017\/1151 (June 2017), http:\/\/data.europa.eu\/eli\/reg\/2017\/1151\/oj"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Tutuianu, M., Bonnel, P., Ciuffo, B., Haniu, T., Ichikawa, N., Marotta, A., Pavlovic, J., Steven, H.: Development of the world-wide harmonized light duty test cycle (wltc) and a possible pathway for its introduction in the european legislation. Transportation Research Part D: Transport and Environment 40(Supplement C), 61 \u2013 75 (2015). https:\/\/doi.org\/10.1016\/j.trd.2015.07.011","DOI":"10.1016\/j.trd.2015.07.011"},{"key":"4_CR26","unstructured":"United Nations: UN Vehicle Regulations - 1958 Agreement, Revision 2, Addendum 100, Regulation No. 101, Revision 3 \u2014 E\/ECE\/324\/Rev.2\/Add.100\/Rev.3 (2013), http:\/\/www.unece.org\/trans\/main\/wp29\/wp29regs101-120.html"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Volpato, M., Tretmans, J.: Approximate active learning of nondeterministic input output transition systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015). https:\/\/doi.org\/10.14279\/tuj.eceasst.72.1008","DOI":"10.14279\/tuj.eceasst.72.1008"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99429-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:18:20Z","timestamp":1648498700000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99429-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994280","9783030994297"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99429-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fase","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}