{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:11:51Z","timestamp":1746115911488,"version":"3.40.4"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T00:00:00Z","timestamp":1726704000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T00:00:00Z","timestamp":1726704000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG\/SCHU 2479"],"award-info":[{"award-number":["DFG\/SCHU 2479"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"TUHH i3 lab initiative","award":["T-LP-E01-WTM-1801-02"],"award-info":[{"award-number":["T-LP-E01-WTM-1801-02"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2025,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Verifying safety requirements by model checking becomes increasingly important for safety-critical applications. For the validity of such proof in practice, the model needs to capture the actual behavior of the real system, which could be tested by containment checks of real observation traces. Basic equivalence checks, however, are not applicable if the system is only partially or imprecisely observable, if the model abstracts from explicit states with symbolic semantics, or if the checks are not expressible in the logics supported by a model checker. In this article, we solve the problem of observation containment checking in timed automata via reachability checking on tester systems. We introduce the logic <jats:italic>SRL (sequence reachability logic)<\/jats:italic> to express observations as sequences of delayed reachability properties. Through <jats:italic>SBLL<\/jats:italic> (introduced by Aceto et al.) as intermediate logic, we synthesize a set of matcher model templates for partial and imprecise observations and further extend these templates for the case of limited state accessibility in a model. For the obtained matching traces, we define the back-transformation into the original model domain and formally prove the correctness of the transformation. We implemented the observation matching approach, and apply it to a set of 7 demo and 3 case study models with different levels of observability. The results show that all positive and negative observations are correctly classified, and that the most advanced matcher model instance still offers average run times between 0.1 and 1\u00a0s in all but 3 scenarios.<\/jats:p>","DOI":"10.1007\/s10270-024-01205-w","type":"journal-article","created":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T09:02:54Z","timestamp":1726736574000},"page":"411-444","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A model template for reachability-based containment checking of imprecise observations in timed automata"],"prefix":"10.1007","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6907-3369","authenticated-orcid":false,"given":"Sascha","family":"Lehmann","sequence":"first","affiliation":[]},{"given":"Sibylle","family":"Schupp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,19]]},"reference":[{"issue":"4","key":"1205_CR1","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s00165-008-0082-7","volume":"20","author":"R Meyer","year":"2008","unstructured":"Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model checking duration calculus: a practical approach. Formal Aspects Comput. 20(4), 481\u2013505 (2008). https:\/\/doi.org\/10.1007\/s00165-008-0082-7","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"1205_CR2","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/S0304-3975(02)00334-1","volume":"300","author":"L Aceto","year":"2003","unstructured":"Aceto, L., Bouyer, P., Burgue\u00f1o, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoret. Comput. Sci. 300(1), 411\u2013475 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(02)00334-1","journal-title":"Theoret. Comput. Sci."},{"key":"1205_CR3","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal 4.0 (2006)"},{"key":"1205_CR4","doi-asserted-by":"publisher","unstructured":"Havelund, K., Larsen, K., Skou, A.: Formal verification of a power controller using the real-time model checker UPPAAL. In: Proceedings of the 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems. ARTS \u201999, vol. 1601, pp. 277\u2013298 (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_17","DOI":"10.1007\/3-540-48778-6_17"},{"key":"1205_CR5","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice. FMSP \u201998, pp. 7\u201315 (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"issue":"7","key":"1205_CR6","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1109\/TSE.2015.2398877","volume":"41","author":"M Autili","year":"2015","unstructured":"Autili, M., Grunske, L., Lumpe, M., Pelliccione, P., Tang, A.: Aligning qualitative, real-time, and probabilistic property specification patterns using a structured English grammar. IEEE Trans. Softw. Eng. 41(7), 620\u2013638 (2015). https:\/\/doi.org\/10.1109\/TSE.2015.2398877","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1205_CR7","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9.: Observer patterns for real-time systems. In: 2013 18th International Conference on Engineering of Complex Computer Systems, pp. 125\u2013134 (2013). https:\/\/doi.org\/10.1109\/ICECCS.2013.26","DOI":"10.1109\/ICECCS.2013.26"},{"key":"1205_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32469-7_1","author":"N Abid","year":"2013","unstructured":"Abid, N., Dal Zilio, S., Botlan, D.: Real-time specification patterns and tools (2013). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_1","journal-title":"Real-time specification patterns and tools"},{"key":"1205_CR9","doi-asserted-by":"publisher","unstructured":"Konrad, S., Cheng, B.: Real-time specification patterns. In: Proceedings of the 27th International Conference on Software Engineering. ICSE \u201905, pp. 372\u2013381 (2005). https:\/\/doi.org\/10.1109\/ICSE.2005.1553580","DOI":"10.1109\/ICSE.2005.1553580"},{"key":"1205_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2022.107100","volume":"154","author":"T Vogel","year":"2023","unstructured":"Vogel, T., Carwehl, M., Rodrigues, G.N., Grunske, L.: A property specification pattern catalog for real-time system verification with UPPAAL. Inf. Softw. Technol. 154, 107100 (2023). https:\/\/doi.org\/10.1016\/j.infsof.2022.107100","journal-title":"Inf. Softw. Technol."},{"key":"1205_CR11","doi-asserted-by":"publisher","unstructured":"Ulus, D., Ferr\u00e8re, T., Asarin, E., Maler, O.: Timed pattern matching. In: Formal Modeling and Analysis of Timed Systems, pp. 222\u2013236 (2014). https:\/\/doi.org\/10.1007\/978-3-319-10512-3_16","DOI":"10.1007\/978-3-319-10512-3_16"},{"key":"1205_CR12","doi-asserted-by":"publisher","unstructured":"Bakhirkin, A., Ferr\u00e8re, T., Nickovic, D., Maler, O., Asarin, E.: Online timed pattern matching using automata. In: Formal Modeling and Analysis of Timed Systems, pp. 215\u2013232 (2018). https:\/\/doi.org\/10.1007\/978-3-030-00151-3_13","DOI":"10.1007\/978-3-030-00151-3_13"},{"issue":"1","key":"1205_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3517194","volume":"32","author":"M Waga","year":"2022","unstructured":"Waga, M., Andr\u00e9, E., Hasuo, I.: Parametric timed pattern matching. ACM Trans. Softw. Eng. Methodol. 32(1), 1\u201335 (2022). https:\/\/doi.org\/10.1145\/3517194","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1205_CR14","doi-asserted-by":"publisher","unstructured":"Alur, R., Kurshan, R.P., Viswanathan, M.: Membership questions for timed and hybrid automata. In: Proceedings 19th IEEE Real-Time Systems Symposium, pp. 254\u2013263 (1998). https:\/\/doi.org\/10.1109\/REAL.1998.739751","DOI":"10.1109\/REAL.1998.739751"},{"issue":"5","key":"1205_CR15","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s00419-006-0086-9","volume":"77","author":"T Uhl","year":"2007","unstructured":"Uhl, T.: The inverse identification problem and its technical application. Arch. Appl. Mech. 77(5), 325\u2013337 (2007). https:\/\/doi.org\/10.1007\/s00419-006-0086-9","journal-title":"Arch. Appl. Mech."},{"key":"1205_CR16","unstructured":"Bourke, T.P.: Modelling and programming embedded controllers with timed automata and synchronous languages. PhD Thesis, University of New South Wales (2009)"},{"issue":"1","key":"1205_CR17","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S., Probst, D.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11\u201344 (1995). https:\/\/doi.org\/10.1007\/BF01384313","journal-title":"Formal Methods Syst. Des."},{"key":"1205_CR18","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S.: Abstraction for branching time properties. In: Computer Aided Verification, pp. 288\u2013300 (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_29","DOI":"10.1007\/978-3-540-45069-6_29"},{"issue":"5","key":"1205_CR19","doi-asserted-by":"publisher","first-page":"2937","DOI":"10.1007\/s10270-018-00706-9","volume":"18","author":"J Dyck","year":"2019","unstructured":"Dyck, J., Giese, H., Lambers, L.: Automatic verification of behavior preservation at the transformation level for relational model transformation. Softw. Syst. Model. 18(5), 2937\u20132972 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00706-9","journal-title":"Softw. Syst. Model."},{"issue":"1","key":"1205_CR20","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-006-0007-9","volume":"9","author":"C Braunstein","year":"2007","unstructured":"Braunstein, C., Encrenaz, E.: CTL-property transformations along an incremental design process. Int. J. Softw. Tools Technol. Transf. 9(1), 77\u201388 (2007). https:\/\/doi.org\/10.1007\/s10009-006-0007-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1205_CR21","doi-asserted-by":"publisher","unstructured":"Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems. In: Formal Modeling and Analysis of Timed Systems, pp. 226\u2013241 (2005). https:\/\/doi.org\/10.1007\/11603009_18","DOI":"10.1007\/11603009_18"},{"issue":"2","key":"1205_CR22","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/0031-3203(93)90034-T","volume":"26","author":"C-K Lin","year":"1993","unstructured":"Lin, C.-K., Fan, K.-C., Tze-Pa Lee, F.: On-line recognition by deviation-expansion model and dynamic programming matching. Pattern Recogn. 26(2), 259\u2013268 (1993). https:\/\/doi.org\/10.1016\/0031-3203(93)90034-T","journal-title":"Pattern Recogn."},{"key":"1205_CR23","doi-asserted-by":"publisher","unstructured":"Milani, A., Jass\u00f3, J., Suriani, S.: Modeling online user behavior. In: 2008 IEEE International Conference on e-Business Engineering, pp. 736\u2013741 (2008). https:\/\/doi.org\/10.1109\/ICEBE.2008.113","DOI":"10.1109\/ICEBE.2008.113"},{"key":"1205_CR24","doi-asserted-by":"publisher","unstructured":"Krichen, M., Tripakis, S.: Black-box conformance testing for real-time systems. In: Model Checking Software, pp. 109\u2013126 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24732-6_8","DOI":"10.1007\/978-3-540-24732-6_8"},{"key":"1205_CR25","doi-asserted-by":"publisher","unstructured":"Gilbert, D., Hogger, C., Zlatuska, J.: Transforming specifications of observable behaviour into programs. In: Logic Program Synthesis and Transformation\u2014Meta-Programming in Logic, pp. 88\u2013103 (1994). https:\/\/doi.org\/10.1007\/3-540-58792-6_6","DOI":"10.1007\/3-540-58792-6_6"},{"key":"1205_CR26","doi-asserted-by":"publisher","unstructured":"Dragomir, I., Iosti, S., Bozga, M., Bensalem, S.: Designing systems with detection and reconfiguration capabilities: A formal approach. In: Leveraging Applications of Formal Methods, Verification and Validation. Distributed Systems, pp. 155\u2013171 (2018). https:\/\/doi.org\/10.1007\/978-3-030-03424-5_11","DOI":"10.1007\/978-3-030-03424-5_11"},{"key":"1205_CR27","doi-asserted-by":"publisher","unstructured":"Agrawal, M., Stephan, F., Thiagarajan, P.S., Yang, S.: Behavioural approximations for restricted linear differential hybrid automata. In: Hybrid Systems: Computation and Control, pp. 4\u201318 (2006).https:\/\/doi.org\/10.1007\/11730637_4","DOI":"10.1007\/11730637_4"},{"key":"1205_CR28","doi-asserted-by":"publisher","unstructured":"Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Formal Methods and Testing: An Outcome of the FORTEST Network, Revised Selected Papers, pp. 77\u2013117 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78917-8_3","DOI":"10.1007\/978-3-540-78917-8_3"},{"key":"1205_CR29","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K., Legay, A., Nyman, U., Wasowski, A.: ECDAR: An environment for compositional design and analysis of real time systems. In: Automated Technology for Verification and Analysis: 8th International Symposium, pp. 365\u2013370 (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_29","DOI":"10.1007\/978-3-642-15643-4_29"},{"key":"1205_CR30","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Runtime Verification, pp. 165\u2013184 (2019). https:\/\/doi.org\/10.1007\/978-3-030-32079-9_10","DOI":"10.1007\/978-3-030-32079-9_10"},{"key":"1205_CR31","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Hybrid Systems III, pp. 232\u2013243 (1996)","DOI":"10.1007\/BFb0020949"},{"key":"1205_CR32","unstructured":"Lehmann, S.: Uppaal Observation Matcher. https:\/\/github.com\/S-Lehmann\/uppyyl-observation-matcher (2023)"},{"key":"1205_CR33","unstructured":"Lehmann, S.: Uppaal Observation Matcher Experiments. https:\/\/github.com\/S-Lehmann\/uppyyl-observation-matcher-experiments (2023)"},{"key":"1205_CR34","unstructured":"Bengtsson, J.: Clocks, DBMs and states in timed systems. PhD thesis, Uppsala University (2002)"},{"key":"1205_CR35","doi-asserted-by":"publisher","unstructured":"Jensen, H., Larsen, K., Skou, A.: Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL. BRICS Rep. Ser. 3(24) (1996). https:\/\/doi.org\/10.7146\/brics.v3i24.20005","DOI":"10.7146\/brics.v3i24.20005"},{"key":"1205_CR36","doi-asserted-by":"publisher","unstructured":"Lonn, H., Pettersson, P.: Formal verification of a TDMA protocol start-up mechanism. In: Proceedings Pacific Rim International Symposium on Fault-Tolerant Systems, pp. 235\u2013242 (1997). https:\/\/doi.org\/10.1109\/PRFTS.1997.640153","DOI":"10.1109\/PRFTS.1997.640153"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01205-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-024-01205-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-024-01205-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T11:06:52Z","timestamp":1746011212000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-024-01205-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,19]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,4]]}},"alternative-id":["1205"],"URL":"https:\/\/doi.org\/10.1007\/s10270-024-01205-w","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2024,9,19]]},"assertion":[{"value":"14 July 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 May 2024","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 July 2024","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 September 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}