@mastersthesis{MTMT:34021928, title = {Abstraction Techniques for the Analysis and Synthesis of Critical Cyber-Physical System Architectures}, url = {https://m2.mtmt.hu/api/publication/34021928}, author = {Marussy, Kristóf}, publisher = {Budapest University of Technology and Economics}, unique-id = {34021928}, year = {2023}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256} } @inproceedings{MTMT:33648748, title = {Consistent Scene Graph Generation by Constraint Optimization}, url = {https://m2.mtmt.hu/api/publication/33648748}, author = {Chen, Boqi and Marussy, Kristóf and Pilarski, Sebastian and Semeráth, Oszkár and Varró, Dániel}, booktitle = {ASE '22: Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering}, doi = {10.1145/3551349.3560433}, unique-id = {33648748}, year = {2022}, pages = {1-13}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @inproceedings{MTMT:33282155, title = {System architecture synthesis for performability by logic solvers}, url = {https://m2.mtmt.hu/api/publication/33282155}, author = {Földiák, M. and Marussy, Kristóf and Varró, D. and Majzik, István}, booktitle = {MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems}, doi = {10.1145/3550355.3552448}, unique-id = {33282155}, year = {2022}, pages = {43-54}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256} } @article{MTMT:32394785, title = {Automated generation of consistent models using qualitative abstractions and exploration strategies}, url = {https://m2.mtmt.hu/api/publication/32394785}, author = {Babikian, Aren A. and Semeráth, Oszkár and Li, Anqi and Marussy, Kristóf and Varró, Dániel}, doi = {10.1007/s10270-021-00918-6}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {21}, unique-id = {32394785}, issn = {1619-1366}, abstract = {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.}, keywords = {Model generation; Exploration strategy; Partial model; Graph solver; SMT-solver; Numeric solver; Test scenario synthesis}, year = {2022}, eissn = {1619-1374}, pages = {1763-1787}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:31360895, title = {Automated Generation of Consistent Graph Models with Multiplicity Reasoning}, url = {https://m2.mtmt.hu/api/publication/31360895}, author = {Marussy, Kristóf and Semeráth, Oszkár and Varró, Dániel}, doi = {10.1109/TSE.2020.3025732}, journal-iso = {IEEE T SOFTWARE ENG}, journal = {IEEE TRANSACTIONS ON SOFTWARE ENGINEERING}, volume = {48}, unique-id = {31360895}, issn = {0098-5589}, abstract = {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.}, year = {2022}, eissn = {1939-3520}, pages = {1610-1629}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:32589291, title = {Worst-case Execution Time Calculation for Query-based Monitors by Witness Generation}, url = {https://m2.mtmt.hu/api/publication/32589291}, author = {Búr, Márton and Marussy, Kristóf and Meyer, Brett H. and Varró, Dániel}, doi = {10.1145/3471904}, journal-iso = {ACM T EMBED COMPUT S}, journal = {ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS}, volume = {20}, unique-id = {32589291}, issn = {1539-9087}, year = {2021}, eissn = {1558-3465}, pages = {1-36}, orcid-numbers = {Búr, Márton/0000-0003-2702-6174; Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @inproceedings{MTMT:32028453, title = {Tensor-based reliability analysis of complex static fault trees}, url = {https://m2.mtmt.hu/api/publication/32028453}, author = {Szekeres, Dániel and Marussy, Kristóf and Majzik, István}, booktitle = {2021 17th European Dependable Computing Conference (EDCC)}, doi = {10.1109/EDCC53658.2021.00012}, unique-id = {32028453}, abstract = {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.}, year = {2021}, pages = {33-40}, orcid-numbers = {Szekeres, Dániel/0000-0002-2912-028X; Marussy, Kristóf/0000-0002-9135-8256} } @article{MTMT:32028274, title = {Automated Generation of Consistent, Diverse and Structurally Realistic Graph Models}, url = {https://m2.mtmt.hu/api/publication/32028274}, author = {Semeráth, Oszkár and Aren, A. Babikian and Boqi, Chen and Chuning, Li and Marussy, Kristóf and Szárnyas, Gábor and Varró, Dániel}, doi = {10.1007/s10270-021-00884-z}, journal-iso = {SOFTW SYST MODEL}, journal = {SOFTWARE AND SYSTEMS MODELING}, volume = {20}, unique-id = {32028274}, issn = {1619-1366}, abstract = {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.}, year = {2021}, eissn = {1619-1374}, pages = {1713-1734}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @inproceedings{MTMT:31872205, title = {Automated generation of consistent models with structural and attribute constraints}, url = {https://m2.mtmt.hu/api/publication/31872205}, author = {Semeráth, Oszkár and Babikian, Aren A. and Li, Anqi and Marussy, Kristóf and Varró, Dániel}, booktitle = {Proceedings of the 23rd ACM/IEEE International Conference on Model Driven Engineering Languages and Systems}, doi = {10.1145/3365438.3410962}, unique-id = {31872205}, year = {2020}, pages = {187-199}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Varró, Dániel/0000-0002-8790-252X} } @article{MTMT:31374125, title = {Simulation-based Safety Assessment of High-level Reliability Models}, url = {https://m2.mtmt.hu/api/publication/31374125}, author = {Nagy, Simon József and Graics, Bence and Marussy, Kristóf and Vörös, András}, doi = {10.4204/EPTCS.316.9}, journal-iso = {ELECTRON PROC THEOR COMPUT SCI}, journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE}, volume = {316}, unique-id = {31374125}, abstract = {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}, year = {2020}, eissn = {2075-2180}, pages = {240-260}, orcid-numbers = {Graics, Bence/0000-0001-5546-5970; Marussy, Kristóf/0000-0002-9135-8256} }