@article{MTMT:34846752, title = {Generalized Formal Model-Verifier: A Formal Approach for Verifying Static Models}, url = {https://m2.mtmt.hu/api/publication/34846752}, author = {Somogyi, Norbert and Mezei, Gergely}, doi = {10.1007/s42979-024-02808-2}, journal-iso = {SN COMP SCI}, journal = {SN COMPUTER SCIENCE}, volume = {5}, unique-id = {34846752}, issn = {2662-995X}, abstract = {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.}, keywords = {UML; formal verification; OCL; Kripke structure; CTL; Nusmv}, year = {2024}, eissn = {2661-8907} } @inproceedings{MTMT:34533664, title = {Field Types for Deep Characterization in Multi-Level Modeling}, url = {https://m2.mtmt.hu/api/publication/34533664}, author = {Kuhne, T. and Almeida, J.P.A. and Atkinson, C. and Jeusfeld, M.A. and Mezei, Gergely}, booktitle = {2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)}, doi = {10.1109/MODELS-C59198.2023.00105}, unique-id = {34533664}, abstract = {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.}, keywords = {Semantics; Trade off; Economic and social effects; multilevel modeling; Modeling approach; multi-level modeling; two-level models; Semantic difference; attribute definition; attribute definition; Clabjects}, year = {2023}, pages = {639-648} } @inproceedings{MTMT:33533355, title = {Verifying Static Constraints on Models Using General Formal Verification Methods}, url = {https://m2.mtmt.hu/api/publication/33533355}, author = {Somogyi, Norbert and Mezei, Gergely}, booktitle = {Proceedings of the 11th International Conference on Model-Driven Engineering and Software Development}, unique-id = {33533355}, year = {2023} } @inproceedings{MTMT:33533286, title = {The Challenges of Defining and Parsing Multi-Layer DMLA Models}, url = {https://m2.mtmt.hu/api/publication/33533286}, author = {Somogyi, Norbert and Mezei, Gergely}, booktitle = {Proceedings of the 10th International Conference on Model-Driven Engineering and Software Development}, doi = {10.5220/0010918900003119}, unique-id = {33533286}, year = {2022}, pages = {358-363} } @inproceedings{MTMT:33339098, title = {DeepTelos and DMLA-A Contribution to the MULTI 2022 Collaborative Comparison Challenge}, url = {https://m2.mtmt.hu/api/publication/33339098}, author = {Jeusfeld, M. and Mezei, Gergely and Bácsi, S.}, booktitle = {Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings}, doi = {10.1145/3550356.3561602}, unique-id = {33339098}, year = {2022}, pages = {414-423} } @inproceedings{MTMT:33283218, title = {Practical application of the multi-level modeling playground}, url = {https://m2.mtmt.hu/api/publication/33283218}, author = {Somogyi, Ferenc Attila and Mezei, Gergely}, booktitle = {Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings}, doi = {10.1145/3550356.3561556}, unique-id = {33283218}, year = {2022}, pages = {453-457} } @inproceedings{MTMT:33115813, title = {Connections between Language Semantics and the Query-based Compiler Architecture}, url = {https://m2.mtmt.hu/api/publication/33115813}, author = {Lenkefi, Peter and Mezei, Gergely}, booktitle = {Proceedings of the 17th International Conference on Software Technologies}, doi = {10.5220/0011260400003266}, unique-id = {33115813}, abstract = {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.}, keywords = {compilers; Language engineering; memoization; Query-based Compilers}, year = {2022}, pages = {167-174} } @inproceedings{MTMT:32757292, title = {Towards Model Transformation with Structural Level-spanning Patterns}, url = {https://m2.mtmt.hu/api/publication/32757292}, author = {Bácsi, Sándor and Mezei, Gergely}, booktitle = {Proceedings of the 10th International Conference on Model-Driven Engineering and Software Development}, doi = {10.5220/0010918800003119}, unique-id = {32757292}, year = {2022}, pages = {352-357} } @{MTMT:32799748, title = {The MULTI Collaborative Comparison Challenge}, url = {https://m2.mtmt.hu/api/publication/32799748}, author = {Mezei, Gergely and Kuhne, T. and Carvalho, V. and Neumayr, B.}, booktitle = {2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)}, doi = {10.1109/MODELS-C53483.2021.00077}, unique-id = {32799748}, year = {2021}, pages = {495-496} } @{MTMT:32799747, title = {Preface to the 8th International Workshop on Multi-Level Modelling (MULTI 2021)}, url = {https://m2.mtmt.hu/api/publication/32799747}, isbn = {9781665424844}, author = {Neumayr, B. and Mezei, Gergely and Carvalho, V.A.}, booktitle = {2021 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C)}, doi = {10.1109/MODELS-C53483.2021.00076}, unique-id = {32799747}, year = {2021}, pages = {493-494} }