TY - THES AU - Marussy, Kristóf TI - Abstraction Techniques for the Analysis and Synthesis of Critical Cyber-Physical System Architectures PB - Budapesti Műszaki és Gazdaságtudományi Egyetem PY - 2023 UR - https://m2.mtmt.hu/api/publication/34021928 ID - 34021928 LA - English DB - MTMT ER - TY - CHAP AU - Chen, Boqi AU - Marussy, Kristóf AU - Pilarski, Sebastian AU - Semeráth, Oszkár AU - Varró, Dániel ED - Aehnelt, M. ED - Kirste, T. TI - Consistent Scene Graph Generation by Constraint Optimization T2 - ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450394758 T3 - ACM international conference proceeding PY - 2022 SP - 1 EP - 13 PG - 13 DO - 10.1145/3551349.3560433 UR - https://m2.mtmt.hu/api/publication/33648748 ID - 33648748 N1 - Electrical and Computer Engineering, McGill University, Montreal, QC, Canada Department of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary LA - English DB - MTMT ER - TY - CHAP AU - Földiák, M. AU - Marussy, Kristóf AU - Varró, D. AU - Majzik, István ED - Eugene, Syriani ED - Houari, Sahraoui TI - System architecture synthesis for performability by logic solvers T2 - MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450394666 PY - 2022 SP - 43 EP - 54 PG - 12 DO - 10.1145/3550355.3552448 UR - https://m2.mtmt.hu/api/publication/33282155 ID - 33282155 N1 - Budapest University of Technology and Economics, Budapest, Hungary McGill University, Montreal, Canada Export Date: 29 November 2022 LA - English DB - MTMT ER - TY - JOUR AU - Babikian, Aren A. AU - Semeráth, Oszkár AU - Li, Anqi AU - Marussy, Kristóf AU - Varró, Dániel TI - Automated generation of consistent models using qualitative abstractions and exploration strategies JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 21 PY - 2022 IS - 5 SP - 1763 EP - 1787 PG - 25 SN - 1619-1366 DO - 10.1007/s10270-021-00918-6 UR - https://m2.mtmt.hu/api/publication/32394785 ID - 32394785 AB - Automatically synthesizing consistent models is a key prerequisite for many testing scenarios in autonomous driving to ensure a designated coverage of critical corner cases. An inconsistent model is irrelevant as a test case (e.g., false positive); thus, each synthetic model needs to simultaneously satisfy various structural and attribute constraints, which includes complex geometric constraints for traffic scenarios. While different logic solvers or dedicated graph solvers have recently been developed, they fail to handle either structural or attribute constraints in a scalable way. In the current paper, we combine a structural graph solver that uses partial models with an SMT-solver and a quadratic solver to automatically derive models which simultaneously fulfill structural and numeric constraints, while key theoretical properties of model generation like completeness or diversity are still ensured. This necessitates a sophisticated bidirectional interaction between different solvers which carry out consistency checks, decision, unit propagation, concretization steps. Additionally, we introduce custom exploration strategies to speed up model generation. We evaluate the scalability and diversity of our approach, as well as the influence of customizations, in the context of four complex case studies. LA - English DB - MTMT ER - TY - JOUR AU - Marussy, Kristóf AU - Semeráth, Oszkár AU - Varró, Dániel TI - Automated Generation of Consistent Graph Models with Multiplicity Reasoning JF - IEEE TRANSACTIONS ON SOFTWARE ENGINEERING J2 - IEEE T SOFTWARE ENG VL - 48 PY - 2022 IS - 5 SP - 1610 EP - 1629 PG - 20 SN - 0098-5589 DO - 10.1109/TSE.2020.3025732 UR - https://m2.mtmt.hu/api/publication/31360895 ID - 31360895 N1 - Funding Agency and Grant Number: BME-Artificial Intelligence FIKP grant of EMMI (BME FIKP-MI/SC); BME NC TKP2020 grant of NKFIH Hungary; New National Excellence Program of the Ministry for Innovation and Technology from National Research, Development and Innovation Fund [UNKP-20-4]; NSERC [RGPIN-04573-16] Funding text: This work was partially supported by BME-Artificial Intelligence FIKP grant of EMMI (BME FIKP-MI/SC), the BME NC TKP2020 grant of NKFIH Hungary, the UNKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and the NSERC RGPIN-04573-16 project. AB - Advanced tools used in model-based systems engineering (MBSE) frequently represent their models as graphs. In order to test those tools, the automated generation of well-formed (or intentionally malformed) graph models is necessitated which is often carried out by solver-based model generation techniques. In many model generation scenarios, one needs more refined control over the generated unit tests to focus on the more relevant models. Type scopes allow to precisely define the required number of newly generated elements, thus one can avoid the generation of unrealistic and highly symmetric models having only a single type of elements. In this paper, we propose a 3-valued scoped partial modeling formalism, which innovatively extends partial graph models with predicate abstraction and counter abstraction. As a result, well-formedness constraints and multiplicity requirements can be evaluated in an approximated way on incomplete (unfinished) models by using advanced graph query engines with numerical solvers (e.g., IP or LP solvers). Based on the refinement of 3-valued scoped partial models, we propose an efficient model generation algorithm that generates models that are both well-formed and satisfy the scope requirements. We show that the proposed approach scales significantly better than existing SAT-solver techniques or the original graph solver without multiplicity reasoning. We illustrate our approach in a complex design-space exploration case study of collaborating satellites introduced by researchers at NASA JPL. LA - English DB - MTMT ER - TY - JOUR AU - Búr, Márton AU - Marussy, Kristóf AU - Meyer, Brett H. AU - Varró, Dániel TI - Worst-case Execution Time Calculation for Query-based Monitors by Witness Generation JF - ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS J2 - ACM T EMBED COMPUT S VL - 20 PY - 2021 IS - 6 SP - 1 EP - 36 PG - 36 SN - 1539-9087 DO - 10.1145/3471904 UR - https://m2.mtmt.hu/api/publication/32589291 ID - 32589291 LA - English DB - MTMT ER - TY - CHAP AU - Szekeres, Dániel AU - Marussy, Kristóf AU - Majzik, István ED - Michael, Paulitsch ED - Mario, Trapp TI - Tensor-based reliability analysis of complex static fault trees T2 - 2021 17th European Dependable Computing Conference (EDCC) PB - Institute of Electrical and Electronics Engineers (IEEE) CY - Piscataway (NJ) SN - 9781665436724 PY - 2021 SP - 33 EP - 40 PG - 8 DO - 10.1109/EDCC53658.2021.00012 UR - https://m2.mtmt.hu/api/publication/32028453 ID - 32028453 N1 - Export Date: 2 May 2022 AB - Fault Tree Analysis is widely used in the reliability evaluation of critical systems, such as railway and automotive systems, power grids, and nuclear power plants. While there are efficient algorithms for calculating the probability of failure in static fault trees, Mean Time to First Failure (MTFF) evaluation remains challenging due to state space explosion. Recently, structural and symmetry reduction methods were proposed to counteract this phenomenon. However, systems with a large number of different and highly interconnected components preclude the use of reduction techniques. Their MTFF analysis requires the solution of a system of linear equations whose size is exponential in the number of components in the system. In this paper, we propose a solution leveraging Tensor Trains as a compressed vector and matrix representation. We build upon Binary Decision Diagram-based techniques to avoid explicit state space enumeration and use linear equation solvers developed specifically for Tensor Trains to efficiently solve the arising linear systems. As a result, our novel approach complements the existing reduction-based techniques and makes some previously intractable models possible to analyze. We evaluate our approach on an industrial case study adapted from a railway system, and other openly available benchmark models. LA - English DB - MTMT ER - TY - JOUR AU - Semeráth, Oszkár AU - Aren, A. Babikian AU - Boqi, Chen AU - Chuning, Li AU - Marussy, Kristóf AU - Szárnyas, Gábor AU - Varró, Dániel TI - Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 20 PY - 2021 IS - 5 SP - 1713 EP - 1734 PG - 22 SN - 1619-1366 DO - 10.1007/s10270-021-00884-z UR - https://m2.mtmt.hu/api/publication/32028274 ID - 32028274 N1 - MTA-BME Lendület Cyber-Physical Systems Res. Grp. Department of Measurement and Information Systems, Budapest University of Technology and Economics, Magyar tudósok krt. 2, Budapest, 1117, Hungary Department of Electrical and Computer Engineering, McGill University, 3480 Rue University, Montréal, QC H3A 0E9, Canada Cited By :1 Export Date: 9 June 2022 Correspondence Address: Semeráth, O.; MTA-BME Lendület Cyber-Physical Systems Res. Grp. Department of Measurement and Information Systems, Magyar tudósok krt. 2, Hungary; email: semerath@mit.bme.hu Funding details: Natural Sciences and Engineering Research Council of Canada, NSERC, PGSD3-546810-2020, RGPIN-04573-16 Funding details: Fonds de recherche du Québec – Nature et technologies, FRQNT, 272709 Funding details: Nemzeti Kutatási, Fejlesztési és Innovaciós Alap, NKFIA Funding details: Innovációs és Technológiai Minisztérium Funding text 1: We would like to thank all three reviewers for their detailed and insightful feedback. This paper was partially supported by the NSERC RGPIN-04573-16 project, the NSERC PGSD3-546810-2020 scholarship, the McGill Grad Excellence Award-90025, the Fonds de recherche du Québec - Nature et technologies (FRQNT) B1X scholarship (file number: 272709), the ÚNKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and by the NRDI Fund based on the charter of bolster issued by the NRDI Office under the auspices of the Ministry for Innovation and Technology. We would like to thank the Department of Electrical and Computer Engineering, and the School of Computer Science of McGill University for providing resources to run our measurements. During the development of the achievements, we took into consideration the goals set by the Balatonfüred System Science Innovation Cluster and the plans of the “BME Balatonfüred Knowledge Center,” supported by EFOP 4.2.1-16-2017-00021. Funding text 2: We would like to thank all three reviewers for their detailed and insightful feedback. This paper was partially supported by the NSERC RGPIN-04573-16 project, the NSERC PGSD3-546810-2020 scholarship, the McGill Grad Excellence Award-90025, the Fonds de recherche du Qu?bec - Nature et technologies (FRQNT) B1X scholarship (file number: 272709), the ?NKP-20-4 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund, and by the NRDI Fund based on the charter of bolster issued by the NRDI Office under the auspices of the Ministry for Innovation and Technology. We would like to thank the Department of Electrical and Computer Engineering, and the School of Computer Science of McGill University for providing resources to run our measurements. During the development of the achievements, we took into consideration the goals set by the Balatonf?red System Science Innovation Cluster and the plans of the ?BME Balatonf?red Knowledge Center,? supported by EFOP 4.2.1-16-2017-00021. AB - In this paper, we present a novel technique to automatically synthesize consistent, diverse and structurally realistic domain-specific graph models. A graph model is (1) consistent if it is metamodel-compliant and it satisfies the well-formedness constraints of the domain; (2) it is diverse if local neighborhoods of nodes are highly different; and (1) it is structurally realistic if a synthetic graph is at a close distance to a representative real model according to various graph metrics used in network science, databases or software engineering. Our approach grows models by model extension operators using a hill-climbing strategy in a way that (A) ensures that there are no constraint violation in the models (for consistency reasons), while (B) more realistic candidates are selected to minimize a target metric value (wrt. the representative real model). We evaluate the effectiveness of the approach for generating realistic models using multiple metrics for guidance heuristics and compared to other model generators in the context of three case studies with a large set of real human models. We also highlight that our technique is able to generate a diverse set of models, which is a requirement in many testing scenarios. LA - English DB - MTMT ER - TY - CHAP AU - Semeráth, Oszkár AU - Babikian, Aren A. AU - Li, Anqi AU - Marussy, Kristóf AU - Varró, Dániel TI - Automated generation of consistent models with structural and attribute constraints T2 - Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450370196 PY - 2020 SP - 187 EP - 199 PG - 13 DO - 10.1145/3365438.3410962 UR - https://m2.mtmt.hu/api/publication/31872205 ID - 31872205 LA - English DB - MTMT ER - TY - JOUR AU - Nagy, Simon József AU - Graics, Bence AU - Marussy, Kristóf AU - Vörös, András TI - Simulation-based Safety Assessment of High-level Reliability Models JF - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE J2 - ELECTRON PROC THEOR COMPUT SCI VL - 316 PY - 2020 SP - 240 EP - 260 PG - 21 SN - 2075-2180 DO - 10.4204/EPTCS.316.9 UR - https://m2.mtmt.hu/api/publication/31374125 ID - 31374125 AB - Systems engineering approaches use high-level models to capture the architecture and behavior of the system. However, when safety engineers conduct safety and reliability analysis, they have to create formal models, such as fault-trees, according to the behavior described by the high-level engineering models and environmental/fault assumptions. Instead of creating low-level analysis models, our approach builds on engineering models in safety analysis by exploiting the simulation capabilities of recent probabilistic programming and simulation advancements. Thus, it could be applied in accordance with standards and best practices for the analysis of a critical automotive system as part of an industrial collaboration, while leveraging high-level block diagrams and statechart models created by engineers. We demonstrate the applicability of our approach in a case study adapted from the automotive system from the collaboration LA - English DB - MTMT ER -