{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:12Z","timestamp":1776333492696,"version":"3.51.2"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2021,6,17]],"date-time":"2021-06-17T00:00:00Z","timestamp":1623888000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,17]],"date-time":"2021-06-17T00:00:00Z","timestamp":1623888000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010665","name":"H2020 Marie Sk\u0142odowska-Curie Actions","doi-asserted-by":"publisher","award":["798482"],"award-info":[{"award-number":["798482"]}],"id":[{"id":"10.13039\/100010665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2022,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present an automated system repair framework for cyber-physical systems. The proposed framework consists of three main steps: (1) system simulation and fault detection to generate a labeled dataset, (2) identification of the repairable temporal properties leading to the faulty behavior and (3) repairing the system to avoid the occurrence of the cause identified in the second step. We express the cause as a past time signal temporal logic (ptSTL) formula and present an efficient monotonicity-based method to synthesize a ptSTL formula from a labeled dataset. Then, in the third step, we modify the faulty system by removing all behaviors that satisfy the ptSTL formula representing the cause of the fault. We apply the framework to two rich modeling formalisms: discrete-time dynamical systems and timed automata. For both of them, we define repairable formulae, the corresponding repair procedures, and illustrate them over case studies.<\/jats:p>","DOI":"10.1007\/s00236-021-00403-z","type":"journal-article","created":{"date-parts":[[2021,6,17]],"date-time":"2021-06-17T18:02:51Z","timestamp":1623952971000},"page":"183-209","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["An automated system repair framework with signal temporal logic"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3369-5553","authenticated-orcid":false,"given":"Mert","family":"Ergurtuna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9987-635X","authenticated-orcid":false,"given":"Beyazit","family":"Yalcinkaya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5813-9836","authenticated-orcid":false,"given":"Ebru","family":"Aydin Gol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,17]]},"reference":[{"key":"403_CR1","unstructured":"System repair toolbox. https:\/\/gitlab.com\/MertErgurtuna\/system_repair_toolbox"},{"key":"403_CR2","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-38916-0_2","volume-title":"Tests and Proofs","author":"BK Aichernig","year":"2013","unstructured":"Aichernig, B.K., Lorber, F., Ni\u010dkovi\u0107, D.: Time for mutants \u2013 model-based mutation testing with timed automata. In: Veanes, M., Vigan\u00f2, L. (eds.) Tests and Proofs, pp. 20\u201338. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013)"},{"key":"403_CR3","doi-asserted-by":"crossref","unstructured":"Alrajeh, D., Craven, R.: Automated error-detection and repair for compositional software specifications. In: Software Engineering and Formal Methods, pp. 111\u2013127. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-10431-7_9"},{"key":"403_CR4","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)"},{"issue":"2","key":"403_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"403_CR6","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Arcaini, P., Gargantini, A., Radavelli, M.: Repairing Timed Automata Clock Guards Through Abstraction and Testing. In: International Conference on Tests and Proofs, pp. 129\u2013146. Springer (2019)","DOI":"10.1007\/978-3-030-31157-5_9"},{"key":"403_CR7","doi-asserted-by":"crossref","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: Imitator 2.5: A tool for analyzing robustness in scheduling problems. In: D.\u00a0Giannakopoulou, D.\u00a0M\u00e9ry (eds.) FM 2012: Formal Methods, pp. 33\u201336. Springer Berlin Heidelberg, Berlin, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32759-9_6"},{"key":"403_CR8","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-taliro: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 254\u2013257. Springer, Berlin (2011)"},{"key":"403_CR9","doi-asserted-by":"crossref","unstructured":"Asarin, E., Donze, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Proceedings of the Second International Conference on Runtime Verification, RV\u201911, pp. 147\u2013160. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-29860-8_12"},{"issue":"11","key":"403_CR10","doi-asserted-by":"publisher","first-page":"2050177","DOI":"10.1142\/S0218126620501777","volume":"29","author":"SK Aydin","year":"2020","unstructured":"Aydin, S.K., Gol, E.A.: Synthesis of monitoring rules with STL. J. Circ. Syst. Comput. 29(11), 2050177 (2020). https:\/\/doi.org\/10.1142\/S0218126620501777","journal-title":"J. Circ. Syst. Comput."},{"key":"403_CR11","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Deshmukh, J., Donz\u00e9, A., Fainekos, G., Maler, O., Ni\u010dkovi\u0107, D., Sankaranarayanan, S.: Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications, pp. 135\u2013175. Springer Int. Pub., Cambridge (2018)","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"403_CR12","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Manjunath, N., Mariani, L., Mateis, C., Ni\u010dkovi\u0107, D.: Automatic failure explanation in CPS models. In: Software Engineering and Formal Methods, pp. 69\u201386. Springer International Publishing, Cambridge (2019)","DOI":"10.1007\/978-3-030-30446-1_4"},{"key":"403_CR13","doi-asserted-by":"publisher","unstructured":"Cai, C.H., Sun, J., Dobbie, G.: Automatic B-model repair using model checking and machine learning. Automated Software Engineering 26, (2019). https:\/\/doi.org\/10.1007\/s10515-019-00264-4","DOI":"10.1007\/s10515-019-00264-4"},{"issue":"2","key":"403_CR14","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1109\/TCNS.2015.2428471","volume":"3","author":"S Coogan","year":"2016","unstructured":"Coogan, S., Gol, E.A., Arcak, M., Belta, C.: Traffic network control from temporal logic specifications. IEEE Trans. Control Netw. Syst. 3(2), 162\u2013172 (2016)","journal-title":"IEEE Trans. Control Netw. Syst."},{"issue":"4","key":"403_CR15","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u0103ionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"403_CR16","first-page":"382","volume-title":"RV 2013, LNCS 8174","author":"A Donze","year":"2013","unstructured":"Donze, A.: On signal temporal logic. In: Legay, A., Bensalem, S. (eds.) RV 2013, LNCS 8174, pp. 382\u2013383. Springer, Berlin (2013)"},{"key":"403_CR17","doi-asserted-by":"publisher","unstructured":"Ergurtuna, M., Gol, E.A.: An efficient formula synthesis method with past signal temporal logic. IFAC-PapersOnLine 52(11), 43 \u2013 48 (2019). https:\/\/doi.org\/10.1016\/j.ifacol.2019.09.116. 5th IFAC Conference on Intelligent Control and Automation Sciences ICONS 2019","DOI":"10.1016\/j.ifacol.2019.09.116"},{"key":"403_CR18","doi-asserted-by":"publisher","unstructured":"Ernst, G., Arcaini, P., Donze, A., Fainekos, G., Mathesen, L., Pedrielli, G., Yaghoubi, S., Yamagata, Y., Zhang, Z.: Arch-comp 2019 category report: Falsification. In: ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems, EPiC Series in Computing, vol.\u00a061, pp. 129\u2013140. EasyChair (2019). https:\/\/doi.org\/10.29007\/68dk","DOI":"10.29007\/68dk"},{"issue":"42","key":"403_CR19","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret. Comput. Sci."},{"key":"403_CR20","doi-asserted-by":"crossref","unstructured":"Ferr\u00e8re, T., Maler, O., Ni\u010dkovi\u0107, D.: Trace diagnostics using temporal implicants. In: Automated Technology for Verification and Analysis, pp. 241\u2013258. Springer International Publishing, Cambridge (2015)","DOI":"10.1007\/978-3-319-24953-7_20"},{"issue":"1","key":"403_CR21","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1109\/TSE.2017.2755013","volume":"45","author":"L Gazzola","year":"2019","unstructured":"Gazzola, L., Micucci, D., Mariani, L.: Automatic software repair: A survey. IEEE Trans. Software Eng. 45(1), 34\u201367 (2019)","journal-title":"IEEE Trans. Software Eng."},{"key":"403_CR22","doi-asserted-by":"crossref","unstructured":"Guha, S., Narayan, C., Arun-Kumar, S.: Reducing clocks in timed automata while preserving bisimulation. In: International Conference on Concurrency Theory, pp. 527\u2013543. Springer, Berlin (2014)","DOI":"10.1007\/978-3-662-44584-6_36"},{"key":"403_CR23","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/3-540-45319-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Hune","year":"2001","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.: Linear parametric model checking of timed automata. In: Margaria, T., Yi, W. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 189\u2013203. Springer, Berlin (2001)"},{"key":"403_CR24","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/s10703-019-00332-1","volume":"54","author":"S Jha","year":"2019","unstructured":"Jha, S., Tiwari, A., Seshia, S.A., Sahai, T., Shankar, N.: Telex: learning signal temporal logic from positive examples using tightness metric. Form. Methods Syst. Des. 54, 364\u2013387 (2019)","journal-title":"Form. Methods Syst. Des."},{"issue":"11","key":"403_CR25","doi-asserted-by":"publisher","first-page":"1704","DOI":"10.1109\/TCAD.2015.2421907","volume":"34","author":"X Jin","year":"2015","unstructured":"Jin, X., Donze, A., Deshmukh, J.V., Seshia, S.A.: Mining requirements from closed-loop control models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34(11), 1704\u20131717 (2015)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"403_CR26","doi-asserted-by":"crossref","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Clock bound repair for timed systems. In: International Conference on Computer Aided Verification, pp. 79\u201396. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-25540-4_5"},{"key":"403_CR27","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-030-53288-8_25","volume-title":"Computer Aided Verification","author":"M K\u00f6lbl","year":"2020","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Tartar: A timed automata repair tool. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification, pp. 529\u2013540. Springer International Publishing, Cham (2020)"},{"key":"403_CR28","doi-asserted-by":"publisher","unstructured":"Liu, B., Lucia, Nejati, S., Briand, L.C., Bruckmann, T.: Simulink fault localization: an iterative statistical debugging approach. Softw. Test. Verif. Reliab. 26(6), 431\u2013459 (2016). https:\/\/doi.org\/10.1002\/stvr.1605","DOI":"10.1002\/stvr.1605"},{"key":"403_CR29","volume-title":"Practical Model-Based Testing: A Tools Approach","author":"BL Mark Utting","year":"2006","unstructured":"Mark Utting, B.L.: Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, Burlington (2006)"},{"key":"403_CR30","unstructured":"MATLAB: version (R2016b). The MathWorks Inc., Natick, Massachusetts (2016)"},{"key":"403_CR31","doi-asserted-by":"publisher","unstructured":"Mohammadinejad, S., Deshmukh, J.V., Puranic, A.G., Vazquez-Chanlatte, M., Donz\u00e9, A.: Interpretable classification of time-series data using efficient enumerative techniques. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC \u201920. ACM, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3365365.3382218","DOI":"10.1145\/3365365.3382218"},{"key":"403_CR32","doi-asserted-by":"crossref","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: Semfix: Program repair via semantic analysis. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE \u201913, pp. 772\u2013781. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"403_CR33","doi-asserted-by":"crossref","unstructured":"Raman, V., Donze, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC \u201915, pp. 239\u2013248. ACM, New York, NY, USA (2015)","DOI":"10.1145\/2728606.2728628"},{"key":"403_CR34","doi-asserted-by":"crossref","unstructured":"Saglam, I., Gol, E.A.: Cause mining and controller synthesis with STL. In: 58th IEEE Conference on Decision and Control (CDC), pp. 4589\u20134594 (2019)","DOI":"10.1109\/CDC40024.2019.9029894"},{"issue":"11","key":"403_CR35","doi-asserted-by":"publisher","first-page":"4142","DOI":"10.1109\/TCAD.2020.3012862","volume":"39","author":"NK Singh","year":"2020","unstructured":"Singh, N.K., Saha, I.: Specification-guided automated debugging of CPS models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 39(11), 4142\u20134153 (2020). https:\/\/doi.org\/10.1109\/TCAD.2020.3012862","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"403_CR36","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-63387-9_15","volume-title":"Computer Aided Verification","author":"M Vazquez-Chanlatte","year":"2017","unstructured":"Vazquez-Chanlatte, M., Deshmukh, J.V., Jin, X., Seshia, S.A.: Logical clustering and learning for time-series data. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification, pp. 305\u2013325. Springer International Publishing, Cambridge (2017)"},{"key":"403_CR37","doi-asserted-by":"publisher","unstructured":"Weimer, W., Nguyen, T., Le\u00a0Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: Proceedings of the 31st International Conference on Software Engineering, ICSE \u201909, p. 364\u2013374. IEEE Computer Society, USA (2009). https:\/\/doi.org\/10.1109\/ICSE.2009.5070536","DOI":"10.1109\/ICSE.2009.5070536"},{"key":"403_CR38","doi-asserted-by":"crossref","unstructured":"Yalcinkaya, B., Gol, E.A.: Clock reduction in timed automata while preserving design parameters. In: 2019 IEEE\/ACM 7th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 31\u201340. IEEE (2019)","DOI":"10.1109\/FormaliSE.2019.00010"},{"key":"403_CR39","unstructured":"Yamagata, Y., Liu, S., Akazaki, T., Duan, Y., Hao, J.: Falsification of cyber-physical systems using deep reinforcement learning. IEEE Transactions on Software Engineering pp. 1\u20131 (2020)"},{"key":"403_CR40","doi-asserted-by":"publisher","unstructured":"Yamaguchi, T., Hoxha, B., Prokhorov, D., Deshmukh, J.V.: Specification-guided software fault localization for autonomous mobile systems. In: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 1\u201312 (2020). https:\/\/doi.org\/10.1109\/MEMOCODE51338.2020.9315067","DOI":"10.1109\/MEMOCODE51338.2020.9315067"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00403-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-021-00403-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-021-00403-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,14]],"date-time":"2022-05-14T09:09:30Z","timestamp":1652519370000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-021-00403-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,17]]},"references-count":40,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2022,6]]}},"alternative-id":["403"],"URL":"https:\/\/doi.org\/10.1007\/s00236-021-00403-z","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,17]]},"assertion":[{"value":"29 September 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 May 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}