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 - CHAP AU - Waudby, Jack AU - Steer, Benjamin A. AU - Karimov, Karim AU - Marton, József AU - Boncz, Peter AU - Szárnyas, Gábor ED - Nambiar, R ED - Poess, M TI - Towards Testing ACID Compliance in the LDBC Social Network Benchmark T2 - Performance Evaluation and Benchmarking PB - Springer Netherlands CY - Cham SN - 9783030849245 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 12752. PY - 2021 SP - 1 EP - 17 PG - 17 DO - 10.1007/978-3-030-84924-5_1 UR - https://m2.mtmt.hu/api/publication/32398430 ID - 32398430 AB - Verifying ACID compliance is an essential part of database benchmarking, because the integrity of performance results can be undermined as the performance benefits of operating with weaker safety guarantees (at the potential cost of correctness) are well known. Traditionally, benchmarks have specified a number of tests to validate ACID compliance. However, these tests have been formulated in the context of relational database systems and SQL, whereas our scope of benchmarking are systems for graph data, many of which are non-relational. This paper presents a set of data model-agnostic ACID compliance tests for the LDBC (Linked Data Benchmark Council) Social Network Benchmark suite's Interactive (SNB-I) workload, a transaction processing benchmark for graph databases. We test all ACID properties with a particular emphasis on isolation, covering 10 transaction anomalies in total. We present results from implementing the test suite on 5 database systems. LA - English DB - MTMT ER - TY - CHAP AU - Szabó, Tamás AU - Erdweg, Sebastian AU - Bergmann, Gábor ED - Stephen, N. Freund ED - Eran, Yahav TI - Incremental whole-program analysis in Datalog with lattices T2 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450383912 PY - 2021 SP - 1 EP - 15 PG - 15 DO - 10.1145/3453483.3454026 UR - https://m2.mtmt.hu/api/publication/32098587 ID - 32098587 AB - Incremental static analyses provide up-to-date analysis results in time proportional to the size of a code change, not the entire code base. This promises fast feedback to programmers in IDEs and when checking in commits. However, existing incremental analysis frameworks fail to deliver on this promise for whole-program lattice-based data-flow analyses. In particular, prior Datalog-based frameworks yield good incremental performance only for intra-procedural analyses. In this paper, we first present a methodology to empirically test if a computation is amenable to incrementalization. Using this methodology, we find that incremental whole-program analysis may be possible. Second, we present a new incremental Datalog solver called LADDDER to eliminate the shortcomings of prior Datalog-based analysis frameworks. Our Datalog solver uses a non-standard aggregation semantics which allows us to loosen monotonicity requirements on analyses and to improve the performance of lattice aggregators considerably. Our evaluation on real-world Java code confirms that LADDDER provides up-to-date points-to, constant propagation, and interval information in milliseconds. 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 - JOUR AU - Bergmann, Gábor TI - Controllable and decomposable multidirectional synchronizations JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 20 PY - 2021 SP - 1735 EP - 1774 PG - 40 SN - 1619-1366 DO - 10.1007/s10270-021-00879-w UR - https://m2.mtmt.hu/api/publication/31965063 ID - 31965063 LA - English DB - MTMT ER - TY - CHAP AU - Elekes, Márton AU - Nagy, Attila AU - Sándor, Dávid AU - Antal, János Benjamin AU - Davis, Timothy A. AU - Szárnyas, Gábor ED - IEEE, null TI - A GraphBLAS solution to the SIGMOD 2014 Programming Contest using multi-source BFS T2 - 2020 IEEE High Performance Extreme Computing Conference (HPEC) PB - IEEE CY - Piscataway (NJ) SN - 9781728192192 PY - 2020 SP - 1 EP - 7 PG - 7 DO - 10.1109/HPEC43674.2020.9286186 UR - https://m2.mtmt.hu/api/publication/31861479 ID - 31861479 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 - TY - JOUR AU - Marussy, Kristóf AU - Semeráth, Oszkár AU - Aren, A. Babikian AU - Varró, Dániel TI - A specification language for consistent model generation based on partial models JF - JOURNAL OF OBJECT TECHNOLOGY J2 - J OBJECT TECHNOL VL - 19 PY - 2020 IS - 3 SP - 1 EP - 22 PG - 22 SN - 1660-1769 DO - 10.5381/jot.2020.19.3.a12 UR - https://m2.mtmt.hu/api/publication/31361799 ID - 31361799 LA - English DB - MTMT ER - TY - CHAP AU - Waudby, Jack AU - Steer, Benjamin A. AU - Prat-Pérez, Arnau AU - Szárnyas, Gábor ED - Akhil, Arora ED - Semih, Salihoglu ED - Nikolay, Yakovets TI - Supporting Dynamic Graphs and Temporal Entity Deletions in the LDBC Social Network Benchmark's Data Generator T2 - Proceedings of the 3rd Joint International Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA) PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450380218 PY - 2020 SP - 1 EP - 8 PG - 8 DO - 10.1145/3398682.3399165 UR - https://m2.mtmt.hu/api/publication/31344297 ID - 31344297 N1 - Alibaba; et al.; IBM; Neo4j; SIGMOD; TigerGraph Conference code: 160983 Cited By :8 Export Date: 7 February 2024 Funding details: FK-128981 Funding details: Alan Turing Institute, EP/T001569/1 Funding details: Engineering and Physical Sciences Research Council, EPSRC, EP/L015358/1 Funding details: Nemzeti Kutatási Fejlesztési és Innovációs Hivatal, NKFIH Funding text 1: the Development and Innovation Office of Hungary (NKFIH), National Research, grant number FK-128981 Funding text 2: The authors would like to thank Peter Boncz for his suggestions. J. Waudby was supported by the Engineering and Physical Sciences Research Council, Centre for Doctoral Training in Cloud Computing for Big Data [grant number EP/L015358/1]. B. Steer was supported by the Engineering and Physical Sciences Research Council and Alan Turing Institute [grant number EP/T001569/1]. G. Szárnyas was partially supported by the MTA-BME Lendület Cyber-Physical Systems Research Group. The parameterization of the data generator was determined with input from the the Development and Innovation Office of Hungary (NKFIH), National Research, grant number FK-128981. LA - English DB - MTMT ER - TY - JOUR AU - Graics, Bence AU - Molnár, Vince AU - Vörös, András AU - Majzik, István AU - Varró, Dániel TI - Mixed-Semantics Composition of Statecharts for the Component-Based Design of Reactive Systems JF - SOFTWARE AND SYSTEMS MODELING J2 - SOFTW SYST MODEL VL - 19 PY - 2020 SP - 1483 EP - 1517 PG - 35 SN - 1619-1366 DO - 10.1007/s10270-020-00806-5 UR - https://m2.mtmt.hu/api/publication/31343505 ID - 31343505 N1 - Deptartment of Measurement and Information Systems, Budapest University of Technology and Economics, Budapest, Hungary MTA-BME Lendület Cyber-physical Systems Research Group, Budapest, Hungary Department of Electrical and Computer Engineering, McGill University, Montreal, Canada Cited By :6 Export Date: 9 June 2022 Correspondence Address: Graics, B.; MTA-BME Lendület Cyber-physical Systems Research GroupHungary; email: graics@mit.bme.hu AB - The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous, and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain. LA - English DB - MTMT ER -