TY - JOUR AU - Somogyi, Norbert AU - Mezei, Gergely TI - Generalized Formal Model-Verifier: A Formal Approach for Verifying Static Models JF - SN COMPUTER SCIENCE J2 - SN COMP SCI VL - 5 PY - 2024 IS - 5 PG - 14 SN - 2662-995X DO - 10.1007/s42979-024-02808-2 UR - https://m2.mtmt.hu/api/publication/34846752 ID - 34846752 N1 - Export Date: 10 May 2024 Correspondence Address: Somogyi, N.; Department of Automation and Applied Informatics, Műegyetem rkp. 3, Hungary; email: somogyi.norbert@aut.bme.hu Funding details: European Commission, EC Funding details: Mesterséges Intelligencia Nemzeti Laboratórium, MILAB Funding text 1: Supported by the the European Union project RRF-2.3.1-21-2022-00004 within the framework of the Artificial Intelligence National Laboratory AB - The field of software modeling has gained significant popularity in the last decades. By capturing the static aspects of the software requirements, model-driven engineering eases the development and maintenance of software. However, additional constraints, such as invariants on model elements, that the solution must conform to may be too complex to include in the structure of the model itself. External solutions are often used to describe static constraints on models, the most prevalent approach being the Object Constraint Language (OCL) and its formal variants. This paper proposes the Generalized Formal Model-Verifier (GFMV), which is a general approach for verifying static constraints on software models. GFMV employs different formal verification methods based on Kripke Structures. Kripke Structures are used to capture the static structure of the model, then the constraints are formalized using a first-order branching-time logic, the Computational Tree Logic (CTL). Finally, the NuSMV model checker is reused to verify whether the constraints formalized in CTL hold on the formal Kripke Structure. When compared to existing solutions, GFMV offers increased generality and formal proof that the constraints hold on the model. The expressive power and runtime-scalability of the approach are evaluated on a real-world example model and OCL invariants cited from literature. © The Author(s) 2024. LA - English DB - MTMT ER - TY - CHAP AU - Kuhne, T. AU - Almeida, J.P.A. AU - Atkinson, C. AU - Jeusfeld, M.A. AU - Mezei, Gergely ED - IEEE, , TI - Field Types for Deep Characterization in Multi-Level Modeling T2 - 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C) PB - IEEE CY - Piscataway (NJ) SN - 9798350324983 PY - 2023 SP - 639 EP - 648 PG - 10 DO - 10.1109/MODELS-C59198.2023.00105 UR - https://m2.mtmt.hu/api/publication/34533664 ID - 34533664 N1 - Conference code: 195746 Export Date: 26 January 2024 Funding details: 2022-2.1.1-NL-2022-00012 Funding details: Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, 313687/2020–0 Funding details: Fundação de Amparo à Pesquisa e Inovação do Espírito Santo, FAPES, 1022/2022, 281/2021 Funding text 1: Gergely Mezei is supported by the Ministry of Culture and Innovation and the National Research, Developmentand Innovation Office (Grant No. 2022-2.1.1-NL-2022-00012). João Paulo A. Almeida is supported by CNPq (Grant No. 313687/2020–0) and FAPES(Grants No. 281/2021, 1022/2022). AB - Traditional two-level modeling approaches distin-guish between class- and object features. Using UML parlance, classes have attributes which require their instances to have object slots. Multi-Level Modeling unifies classes and objects to 'clabjects', and it has been suggested that attributes and slots can and should be unified to 'fields' in a similar way. The notion of deep instantiation for clabjects creates the possibility of 'deep fields', i.e., fields that expand on the roles of pure attributes or pure slots. In this paper, we discuss several variants of such a 'deep field' notion, pointing out the semantic differences and the various resulting trade-offs. We hope our observations will help clarify the range of options for supporting clabject fields in multi-level modeling and thus aid future MLM development. © 2023 IEEE. LA - English DB - MTMT ER - TY - CHAP AU - Somogyi, Norbert AU - Mezei, Gergely ED - Pires, Luís Ferreira ED - Hammoudi, Slimane ED - Seidewitz, Edwin TI - Verifying Static Constraints on Models Using General Formal Verification Methods T2 - Proceedings of the 11th International Conference on Model-Driven Engineering and Software Development PB - SciTePress CY - Setubal PY - 2023 UR - https://m2.mtmt.hu/api/publication/33533355 ID - 33533355 N1 - Accepted for publication. LA - English DB - MTMT ER - TY - CHAP AU - Somogyi, Norbert AU - Mezei, Gergely TI - The Challenges of Defining and Parsing Multi-Layer DMLA Models T2 - Proceedings of the 10th International Conference on Model-Driven Engineering and Software Development SN - 9789897585500 PY - 2022 SP - 358 EP - 363 PG - 6 DO - 10.5220/0010918900003119 UR - https://m2.mtmt.hu/api/publication/33533286 ID - 33533286 N1 - Export Date: 13 October 2023 LA - English DB - MTMT ER - TY - CHAP AU - Jeusfeld, M. AU - Mezei, Gergely AU - Bácsi, S. TI - DeepTelos and DMLA-A Contribution to the MULTI 2022 Collaborative Comparison Challenge T2 - Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450394673 PY - 2022 SP - 414 EP - 423 PG - 10 DO - 10.1145/3550356.3561602 UR - https://m2.mtmt.hu/api/publication/33339098 ID - 33339098 N1 - School of Informatics (IIT), University of Skovde, Skovde, Sweden Dep. of Aut. and Applied Informatics, Budapest Uni. of Tech. and Economics, Budapest, Hungary Export Date: 15 December 2022 LA - English DB - MTMT ER - TY - CHAP AU - Somogyi, Ferenc Attila AU - Mezei, Gergely TI - Practical application of the multi-level modeling playground T2 - Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings PB - Association for Computing Machinery (ACM) CY - New York, New York SN - 9781450394673 PY - 2022 SP - 453 EP - 457 PG - 5 DO - 10.1145/3550356.3561556 UR - https://m2.mtmt.hu/api/publication/33283218 ID - 33283218 N1 - Export Date: 15 December 2022 LA - English DB - MTMT ER - TY - CHAP AU - Lenkefi, Peter AU - Mezei, Gergely ED - Hans-Georg, Fill ED - Marten, van Sinderen ED - Leszek, Maciaszek TI - Connections between Language Semantics and the Query-based Compiler Architecture T2 - Proceedings of the 17th International Conference on Software Technologies PB - SciTePress CY - Setubal SN - 9789897585883 T3 - ICSOFT - International Conference on Software Technologies, ISSN 2184-2833 PY - 2022 SP - 167 EP - 174 PG - 8 DO - 10.5220/0011260400003266 UR - https://m2.mtmt.hu/api/publication/33115813 ID - 33115813 N1 - Funding Agency and Grant Number: National Research, Development and Innovation Fund of Hungary [2019-1.1.1-PIACI-KFI-2019-00263]; [2019-1.1] Funding text: The work presented in this paper has been carried out in the frame of project no. 2019-1.1.1-PIACI-KFI-2019-00263, which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the 2019-1.1. funding scheme. AB - Modern software development has drastically changed the role of compilers with the introduction of responsive development tools. To accommodate this change, compilers have to go through an architectural transformation, diverging from the classic pipeline. A relatively new idea is called query-based compiler design, which took inspiration from build systems. It splits up the pipeline into smaller, individual operations, which - given some constraints - allows for some interesting optimizations. We argue that some programming language semantics introduce cyclic dependencies between certain compiler passes, which can naturally lead to rediscovering query-based compilers. In this paper, we present a framework that can be used to create compilers with a query-based architecture. Based on this framework, we introduce the Yoakke programming language, which we also use to explore our hypothesis regarding cyclic dependencies and rediscovering query-based compilers. LA - English DB - MTMT ER - TY - CHAP AU - Bácsi, Sándor AU - Mezei, Gergely TI - Towards Model Transformation with Structural Level-spanning Patterns T2 - Proceedings of the 10th International Conference on Model-Driven Engineering and Software Development SN - 9789897585500 PY - 2022 SP - 352 EP - 357 PG - 6 DO - 10.5220/0010918800003119 UR - https://m2.mtmt.hu/api/publication/32757292 ID - 32757292 N1 - Export Date: 13 October 2023 LA - English DB - MTMT ER - TY - CHAP AU - Mezei, Gergely AU - Kuhne, T. AU - Carvalho, V. AU - Neumayr, B. ED - IEEE, Computer Society TI - The MULTI Collaborative Comparison Challenge T2 - 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C) PB - IEEE Computer Society Press CY - Los Alamitos (CA) SN - 9781665424844 PY - 2021 SP - 495 EP - 496 PG - 2 DO - 10.1109/MODELS-C53483.2021.00077 UR - https://m2.mtmt.hu/api/publication/32799748 ID - 32799748 N1 - Export Date: 29 April 2022 LA - English DB - MTMT ER - TY - CHAP AU - Neumayr, B. AU - Mezei, Gergely AU - Carvalho, V.A. ED - IEEE, Computer Society TI - Preface to the 8th International Workshop on Multi-Level Modelling (MULTI 2021) T2 - 2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C) PB - IEEE Computer Society Press CY - Los Alamitos (CA) SN - 9781665424844 PY - 2021 SP - 493 EP - 494 PG - 2 SN - 9781665424844 DO - 10.1109/MODELS-C53483.2021.00076 UR - https://m2.mtmt.hu/api/publication/32799747 ID - 32799747 N1 - Export Date: 29 April 2022 LA - English DB - MTMT ER -