@article{MTMT:36855049,
	title = {Aiding the design of critical software systems by iterative exploration of distinct requirement violation scenarios},
	url = {https://m2.mtmt.hu/api/publication/36855049},
	author = {Szabó, Richárd and Szekeres, Dániel and Nagy, Simon József and Thimár, Zoltán and Majzik, István and Micskei, Zoltán Imre and Vörös, András},
	doi = {10.1007/s10664-025-10786-z},
	journal-iso = {EMPIR SOFTW ENG},
	journal = {EMPIRICAL SOFTWARE ENGINEERING},
	volume = {31},
	unique-id = {36855049},
	issn = {1382-3256},
	abstract = {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.},
	year = {2026},
	eissn = {1573-7616},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332; Szekeres, Dániel/0000-0002-2912-028X; Micskei, Zoltán Imre/0000-0003-1846-261X}
}

@article{MTMT:37018585,
	title = {Data-driven Decision Support in Custom Manufacturing Planning},
	url = {https://m2.mtmt.hu/api/publication/37018585},
	author = {Szabó, Richárd and Gönczy, László and Mikó, Balázs and Nagy, Dániel},
	doi = {10.3311/PPme.38356},
	journal-iso = {PERIOD POLYTECH MECH ENG},
	journal = {PERIODICA POLYTECHNICA-MECHANICAL ENGINEERING},
	volume = {70},
	unique-id = {37018585},
	issn = {0324-6051},
	abstract = {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.},
	year = {2026},
	eissn = {1587-379X},
	pages = {1-16},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332; Mikó, Balázs/0000-0003-3609-0290}
}

@inproceedings{MTMT:36196264,
	title = {Towards Configurable Coordination for Distributed Reactive Systems},
	url = {https://m2.mtmt.hu/api/publication/36196264},
	author = {Szabó, Richárd and Cziborová, Dóra and Vörös, András},
	booktitle = {Proceedings of the 32nd Minisymposium},
	doi = {10.3311/MINISY2025-009},
	unique-id = {36196264},
	abstract = {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.},
	year = {2025},
	pages = {45-50},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:36408410,
	title = {Automata-based representation of coordination for distributed reactive systems},
	url = {https://m2.mtmt.hu/api/publication/36408410},
	author = {Szabó, Richárd and Cziborová, Dóra},
	booktitle = {Proceedings of the International Conference on Formal Methods and Foundations of Artificial Intelligence},
	doi = {10.17048/fmfai.2025.201},
	unique-id = {36408410},
	abstract = {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.},
	year = {2025},
	pages = {201-213},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:34872818,
	title = {Modeling of Time-Dependent Behavior in Fault-Tolerant Systems},
	url = {https://m2.mtmt.hu/api/publication/34872818},
	author = {Cziborová, Dóra and Szabó, Richárd},
	booktitle = {Proceedings of the 31th Minisymposium},
	doi = {10.3311/MINISY2024-011},
	unique-id = {34872818},
	year = {2024},
	pages = {55-60},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:32679018,
	title = {Dependability Modeling of Cyber-Physical Systems in the Gamma Framework},
	url = {https://m2.mtmt.hu/api/publication/32679018},
	author = {Szabó, Richárd and Vörös, András},
	booktitle = {Proceedings of the 29th Minisymposium of the Department of Measurement and Information Systems Budapest University of Technology and Economics},
	unique-id = {32679018},
	year = {2022},
	pages = {20-23},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:32678847,
	title = {Demonstrator for dependable edge-based cyber-physical systems},
	url = {https://m2.mtmt.hu/api/publication/32678847},
	author = {Nagy, Simon József and Szabó, Richárd and Vajda, Mate Levente and Vörös, András},
	booktitle = {2021 10th Latin-American Symposium on Dependable Computing (LADC)},
	doi = {10.1109/LADC53747.2021.9672569},
	unique-id = {32678847},
	year = {2021},
	pages = {1-8},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@inproceedings{MTMT:32678929,
	title = {Towards formally analyzed Cyber-Physical Systems},
	url = {https://m2.mtmt.hu/api/publication/32678929},
	author = {Szabó, Richárd and Vörös, András},
	booktitle = {Student Forum Proceedings- EDCC 2021},
	unique-id = {32678929},
	year = {2021},
	pages = {1-4},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332}
}

@CONFERENCE{MTMT:30704172,
	title = {Design and Implementation of a Dependable, Smart CPS Demonstrator},
	url = {https://m2.mtmt.hu/api/publication/30704172},
	author = {Szabó, Richárd and Mázló, Zsolt and Vörös, András and Pataricza, András},
	booktitle = {Conference on Software Technology and Cyber Security},
	unique-id = {30704172},
	year = {2019},
	pages = {1},
	orcid-numbers = {Szabó, Richárd/0000-0003-1307-3332; Pataricza, András/0000-0002-6516-129X}
}