TY - JOUR AU - Graics, Bence AU - Molnár, Vince AU - Majzik, István TI - Integration test generation for state-based components in the Gamma framework JF - INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING: A NASA JOURNAL J2 - INNOV SYST SOFTW ENG (NASA) VL - 22 PY - 2026 IS - 2 PG - 34 SN - 1614-5046 DO - 10.1007/s11334-026-00643-7 UR - https://m2.mtmt.hu/api/publication/37445853 ID - 37445853 N1 - This work was partially supported by the ÚNKP-20-3 New National Excellence Program of the Ministry for Innovation and Technology. Open access funding provided by Budapest University of Technology and Economics. AB - Nowadays, the design of complex reactive systems, e.g., control systems in the railway and aerospace industries, is generally based on the integration of components. Components (subsystems) may come from various parties and operate according to different execution and interaction semantics. Analyzing the joint behavior of such integrated components is a tedious task. This paper introduces a model-based approach in our Gamma Statechart Composition Framework for integration test generation on the basis of collaborating state-based models. Test generation is supported by test coverage criteria and the automatic transformation of composite models into different model checker back-ends. The diagnostic traces returned by the model checkers are automatically mapped into test cases. As novelty, our tool is based on precise composition semantics (synchronous and asynchronous) and relies on model queries to support the modular and flexible specification of element coverage according to various model-based criteria: dataflow, component interactions and static model elements. The tool utilizes model reduction and slicing techniques during the transformations to ease test generation complexity using query-dependent model processing. We demonstrate the applicability of our tool on three industrial subsystems, including an aerospace (NASA) and two railway applications. LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Mondok, Milán AU - Molnár, Vince AU - Majzik, István TI - Model-based testing of asynchronously communicating distributed controllers using validated mappings to formal representations JF - SCIENCE OF COMPUTER PROGRAMMING J2 - SCI COMPUT PROGRAM VL - 242 PY - 2025 PG - 40 SN - 0167-6423 DO - 10.1016/j.scico.2025.103265 UR - https://m2.mtmt.hu/api/publication/35730361 ID - 35730361 N1 - Export Date: 3 February 2025 CODEN: SCPGD Correspondence Address: Graics, B.; Budapest University of Technology and Economics, Műegyetem rkp. 3., Hungary; email: graics@mit.bme.hu LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Mondok, Milán AU - Molnár, Vince AU - Majzik, István TI - Model-Based Testing of Asynchronously Communicating Distributed Controllers JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14485 PY - 2024 SP - 23 EP - 44 PG - 22 SN - 0302-9743 DO - 10.1007/978-3-031-52183-6_2 UR - https://m2.mtmt.hu/api/publication/34504488 ID - 34504488 N1 - Conference code: 306759 Export Date: 19 February 2024 Correspondence Address: Graics, B.; Department of Measurement and Information Systems, Műegyetem rkp. 3., Hungary; email: graics@mit.bme.hu LA - English DB - MTMT ER - TY - CHAP AU - Molnár, Vince AU - Graics, Bence AU - Vörös, András AU - Tonetta, Stefano AU - Cristoforetti, Luca AU - Kimberly, Greg AU - Dyer, Pamela AU - Giammarco, Kristin AU - Koethe, Manfred AU - Hester, John AU - Smith, Jamie AU - Grimm, Christoph TI - Towards the Formal Verification of SysML v2 Models T2 - MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9798400706226 PY - 2024 SP - 1086 EP - 1095 PG - 10 DO - 10.1145/3652620.3687820 UR - https://m2.mtmt.hu/api/publication/35500643 ID - 35500643 N1 - Funding Agency and Grant Number: German BMBF [2022-1.2.4-EUREKA-2023-00013, 2022-1.2.4-EUREKA] Funding text: We would like to thank every member of the Formal Methods Working Group who helped us write this paper with their insights and comments. We are also grateful to Ed Seidewitz and Conrad Bock, who never get tired of answering our questions. SysMD received support (GENIAL, KI4BoardNet) from the German BMBF. Gamma received support project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4-EUREKA funding scheme. LA - English DB - MTMT ER - TY - CHAP AU - Graics, Bence AU - Majzik, István TI - Integration Test Generation and Formal Verification for Distributed Controllers T2 - 30th Minisymposium of the Department of Measurement and Information Systems PB - Budapest University of Technology and Economics CY - Budapest SN - 9789634219040 PY - 2023 SP - 1 EP - 4 PG - 4 UR - https://m2.mtmt.hu/api/publication/33689503 ID - 33689503 LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Molnár, Vince AU - Majzik, István TI - Component‐based specification, design and verification of adaptive systems JF - SYSTEMS ENGINEERING J2 - SYSTEMS ENG VL - 26 PY - 2023 IS - 5 SP - 567 EP - 589 PG - 23 SN - 1098-1241 DO - 10.1002/sys.21675 UR - https://m2.mtmt.hu/api/publication/33739468 ID - 33739468 N1 - Funding Agency and Grant Number: New National Excellence Program of the Ministry for Innovation and Technology [2019-2.1.1-EUREKA-2019-00001, TKP2021-EGA-02]; National Research, Development and Innovation Fund of Hungary [2019-2.1.1-EUREKA-2019-00001, TKP2021-EGA-02]; New National Excellence Program of the Ministry for Innovation and Technology [UNKP-20-3-I-BME-42, UNKP-22-3-II-BME-223] Funding text: National Research, Development and Innovation Fund of Hungary, Grant/Award Numbers: 2019-2.1.1-EUREKA-2019-00001, TKP2021-EGA-02; New National Excellence Program of the Ministry for Innovation and Technology, Grant/Award Numbers: UNKP-20-3-I-BME-42, UNKP-22-3-II-BME-223 LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Molnár, Vince AU - Majzik, István TI - Configurable Model-Based Test Generation for Distributed Controllers Using Declarative Model Queries and Model Checkers JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14290 PY - 2023 SP - 76 EP - 95 PG - 20 SN - 0302-9743 DO - 10.1007/978-3-031-43681-9_5 UR - https://m2.mtmt.hu/api/publication/34144059 ID - 34144059 N1 - Export Date: 26 October 2023 Correspondence Address: Graics, B.; Department of Measurement and Information Systems, Műegyetem rkp. 3., Hungary; email: graics@mit.bme.hu LA - English DB - MTMT ER - TY - THES AU - Graics, Bence TI - Formal modeling, verification and test generation for component-based reactive systems PB - Budapesti Műszaki és Gazdaságtudományi Egyetem PY - 2023 SP - 195 UR - https://m2.mtmt.hu/api/publication/35433228 ID - 35433228 LA - English DB - MTMT ER - TY - JOUR AU - Horváth, Benedek AU - Molnár, Vince AU - Graics, Bence AU - Hajdu, Ákos AU - Ráth, István Zoltán AU - Horváth, Ákos AU - Karban, Robert AU - Trancho, Gelys AU - Micskei, Zoltán Imre TI - Pragmatic verification and validation of industrial executable SysML models JF - SYSTEMS ENGINEERING J2 - SYSTEMS ENG VL - 26 PY - 2023 IS - 6 SP - 693 EP - 714 PG - 22 SN - 1098-1241 DO - 10.1002/sys.21679 UR - https://m2.mtmt.hu/api/publication/33809830 ID - 33809830 N1 - IncQuery Labs cPlc., Budapest, Hungary Department of Business Informatics - Software Engineering, Johannes Kepler University Linz, Linz, Austria Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, United States TMT International Observatory LLC, Pasadena, CA, United States Export Date: 26 May 2023 Correspondence Address: Horváth, B.; IncQuery Labs cPlcHungary; email: benedek.horvath@incquerylabs.com LA - English DB - MTMT ER - TY - CHAP AU - Csuvarszki, János Csanád AU - Graics, Bence AU - Vörös, András ED - Renczes, Balázs TI - Model-Driven Development of Heterogeneous Cyber-Physical Systems T2 - Proceedings of the 28th PhD Mini-Symposium PB - BME Méréstechnika és Információs Rendszerek Tanszék CY - Budapest SN - 9789634218456 PY - 2021 SP - 24 EP - 27 PG - 4 UR - https://m2.mtmt.hu/api/publication/31868691 ID - 31868691 AB - Cyber-physical systems (CPS) are becoming more prevalent for the reliable execution of critical tasks, e.g., in the aerospace and medical fields. The development of such systems is challenging, due to the heterogeneity of the components ranging from sensors and embedded controllers to cloud solutions. Model-driven approaches can provide a high-level abstraction to combat the challenges. This paper proposes a model-driven development approach supporting the precise modeling of CPS and the automatic derivation of implementation from the resulting models. The approach introduces a composition semantics tailored to heterogeneous architectures for the precise description of component interactions. Automated code generators allow the execution of standalone software components on real-time controllers and support the synthesis of standalone hardware components, enabling both the derivation of embedded software and the description of logical circuit behavior. Component interactions are supported by multiple communication solutions generally used in critical, real-time embedded systems. The approach is implemented in the Gamma framework and its applicability is demonstrated in two case studies. LA - English DB - MTMT ER -