TY - JOUR AU - Szabó, Richárd AU - Szekeres, Dániel AU - Nagy, Simon József AU - Thimár, Zoltán AU - Majzik, István AU - Micskei, Zoltán Imre AU - Vörös, András TI - Aiding the design of critical software systems by iterative exploration of distinct requirement violation scenarios JF - EMPIRICAL SOFTWARE ENGINEERING J2 - EMPIR SOFTW ENG VL - 31 PY - 2026 IS - 3 PG - 52 SN - 1382-3256 DO - 10.1007/s10664-025-10786-z UR - https://m2.mtmt.hu/api/publication/36855049 ID - 36855049 N1 - Financial support was received from the following grants: Project no. 2019-1.3.1-KK-2019-00004 has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the 2019-1.3.1-KK funding scheme. The project supported by the Doctoral Excellence Fellowship Programme (DCEP) is funded by the National Research Development and Innovation Fund of the Ministry of Culture and Innovation and the Budapest University of Technology and Economics, under a grant agreement with the National Research, Development and Innovation Office. This research was partially funded by the 2024-2.1.1-EKÖP-2024-00003 University Research Scholarship Programme under project number EKÖP-24-3-BME-159 with the support provided by the Ministry of Culture and Innovation of Hungary from the NRDI Fund. AB - Fault-tolerant behavior is prevalent in many fields of critical software systems. The complexity of such systems necessitates rigorous techniques for ensuring correct and reliable operation. Performing design reviews by experts is the conventional method in the industry, but it is hard to substantiate the completeness of the result. We performed a multi-year study with an automotive supplier on supporting standard-mandated safety evaluations with model checking in the context of a critical steer-by-wire function. However, existing formal verification methods returned too many redundant violations that the engineers deemed unrealistic or acceptable. Based on these findings, we propose a new process focusing on systematic, iterative exploration of distinct requirement violation scenarios with model checkers to aid the design and verification of fault-tolerant safety-critical software systems. The main challenge lies in the need to find all essentially distinct problems of subsystems without enumerating the potentially infinitely many problematic execution paths. The novelty of our approach is using abstract scenario descriptions constraining the model checker to unknown violations while allowing some violations to be categorized as acceptable by subject experts. Our approach has multifold benefits: It turns implicit assumptions into formalized environmental models and scenario descriptions, sheds light on hard-to-find requirement violations, and can be integrated into existing development processes. We present the applicability of our approach in the automotive study, where it revealed previously unknown problems in the system design and gave formal proofs to help the engineers negotiate with the client regarding required modifications. LA - English DB - MTMT ER - TY - JOUR AU - Szabó, Richárd AU - Gönczy, László AU - Mikó, Balázs AU - Nagy, Dániel TI - Data-driven Decision Support in Custom Manufacturing Planning JF - PERIODICA POLYTECHNICA-MECHANICAL ENGINEERING J2 - PERIOD POLYTECH MECH ENG VL - 70 PY - 2026 IS - 1 SP - 1 EP - 16 PG - 16 SN - 0324-6051 DO - 10.3311/PPme.38356 UR - https://m2.mtmt.hu/api/publication/37018585 ID - 37018585 N1 - Funding Agency and Grant Number: Doctoral Excellence Fellowship Programme (DCEP) - National Research Development and Innovation Fund of the Ministry of Culture and Innovation; Budapest University of Technology and Economics; National Research, Development and Innovation Office; [GINOP-2.1.2-8-1-4-16-2018-00405] Funding text: This work has been partially supported by the GINOP-2.1.2-8-1-4-16-2018-00405 project. The project supported by the Doctoral Excellence Fellowship Programme (DCEP) is funded by the National Research Development and Innovation Fund of the Ministry of Culture and Innovation and the Budapest University of Technology and Economics, under a grant agreement with the National Research, Development and Innovation Office. The authors express their gratitude to the colleagues who helped them in the writing of this publication: Dr. Andras V8r8s and Dr. Oszkar Semerath from BME. The authors would also like to thank all former colleagues at BME, Quanopt, and Component Ltd. who helped with the implementation of the methods described. AB - In the design for manufacturing, the choice of the best processing activities and production scheduling plays an important role. The aim of the research is to create an automated process estimation system based on the processing plan of previously manufactured artifacts, which supports the scheduling software in the case of a custom manufacturing environment. We present a method and corresponding similarity metrics and evaluate the performance of our method on a set of real-life manufacturing plans and design data. LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Cziborová, Dóra AU - Vörös, András ED - Renczes, Balázs TI - Towards Configurable Coordination for Distributed Reactive Systems T2 - Proceedings of the 32nd Minisymposium PB - Budapest University of Technology and Economics, Department of Artificial Intelligence and Systems Engineering CY - Budapest SN - 9789634219897 PY - 2025 SP - 45 EP - 50 PG - 6 DO - 10.3311/MINISY2025-009 UR - https://m2.mtmt.hu/api/publication/36196264 ID - 36196264 AB - Modern cyber-physical systems (CPS) present unique challenges as they are distributed real-time systems used in many critical application domains, such as automotive or railway systems. However, modeling and verifying the distributed and timed aspects of the system are challenging tasks. We need a precise description of the possible orderings of the components' execution, and a formal representation to be able to run formal verification. In this paper, we investigate the possible extension of a modeling and verification framework to support the flexible, configurable description of the coordination of distributed critical systems. We present an extension of the timed automata formalism, the coordination automata formalism, and show the applicability of the extension on a motivating example. LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Cziborová, Dóra ED - Tómács, Tibor TI - Automata-based representation of coordination for distributed reactive systems T2 - Proceedings of the International Conference on Formal Methods and Foundations of Artificial Intelligence PB - Eszterházy Károly Katolikus Egyetem Líceum Kiadó CY - Eger SN - 9789634963035 PY - 2025 SP - 201 EP - 213 PG - 13 DO - 10.17048/fmfai.2025.201 UR - https://m2.mtmt.hu/api/publication/36408410 ID - 36408410 AB - Modern cyber-physical systems (CPS) are distributed reactive real-time systems used in many critical application domains, such as automotive or railway systems, so ensuring their correctness is essential. Formal verification can exhaustively explore the behavior of the formal representation of CPS to ensure its reliability. Engineering modeling tools provide separate modeling constructs for the different aspects of the systems, e.g., behavior, architecture, and scheduling, but lack formal composition, making system-level verification difficult. Formal modeling tools, e.g., Lingua Franca or the Gamma Statechart Composition Framework, are efficient in describing component behavior, and they provide formal composition semantics of the subsystems. However, the provided composition patterns in these languages are not general, so incorporating the precise coordination, scheduling, and interaction aspects requires the modification of the component models by encoding the coordination into the components. In this paper, we present a configurable formal description approach for the coordination of distributed critical systems. We extend the well-known timed automata formalism to coordinate the execution of the components by directly reusing the formal models of the components, making the coordination of the system components a first-class citizen. LA - English DB - MTMT ER - TY - CHAP AU - Cziborová, Dóra AU - Szabó, Richárd TI - Modeling of Time-Dependent Behavior in Fault-Tolerant Systems T2 - Proceedings of the 31th Minisymposium PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219514 PY - 2024 SP - 55 EP - 60 PG - 6 DO - 10.3311/MINISY2024-011 UR - https://m2.mtmt.hu/api/publication/34872818 ID - 34872818 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Vörös, András ED - Renczes, Balázs TI - Dependability Modeling of Cyber-Physical Systems in the Gamma Framework T2 - Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218722 PY - 2022 SP - 20 EP - 23 PG - 4 UR - https://m2.mtmt.hu/api/publication/32679018 ID - 32679018 LA - English DB - MTMT ER - TY - CHAP AU - Nagy, Simon József AU - Szabó, Richárd AU - Vajda, Mate Levente AU - Vörös, András ED - Andrey, Brito ED - Fernando, Pedone TI - Demonstrator for dependable edge-based cyber-physical systems T2 - 2021 10th Latin-American Symposium on Dependable Computing (LADC) PB - Institute of Electrical and Electronics Engineers (IEEE) CY - Piscataway (NJ) SN - 9781665478311 PY - 2021 SP - 1 EP - 8 PG - 8 DO - 10.1109/LADC53747.2021.9672569 UR - https://m2.mtmt.hu/api/publication/32678847 ID - 32678847 LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Richárd AU - Vörös, András TI - Towards formally analyzed Cyber-Physical Systems T2 - Student Forum Proceedings- EDCC 2021 PB - arXiv.org CY - München PY - 2021 SP - 1 EP - 4 PG - 4 UR - https://m2.mtmt.hu/api/publication/32678929 ID - 32678929 LA - English DB - MTMT ER - TY - CONF AU - Szabó, Richárd AU - Mázló, Zsolt AU - Vörös, András AU - Pataricza, András TI - Design and Implementation of a Dependable, Smart CPS Demonstrator T2 - Conference on Software Technology and Cyber Security PY - 2019 SP - 1 UR - https://m2.mtmt.hu/api/publication/30704172 ID - 30704172 LA - English DB - MTMT ER -