@inproceedings{MTMT:34895395, title = {From Hard-Coded to Modeled: Towards Making Semantic-Preserving Model Transformations More Flexible}, url = {https://m2.mtmt.hu/api/publication/34895395}, author = {Zavada, Ármin and Molnár, Vince}, booktitle = {Proceedings of the 31th Minisymposium}, doi = {10.3311/MINISY2024-008}, unique-id = {34895395}, year = {2024}, pages = {41-45}, orcid-numbers = {Zavada, Ármin/0000-0001-7424-8410; Molnár, Vince/0000-0002-8204-7595} } @inproceedings{MTMT:35600740, title = {From Transpilers to Semantic Libraries: Formal Verification With Pluggable Semantics}, url = {https://m2.mtmt.hu/api/publication/35600740}, author = {Zavada, Ármin and Marussy, Kristóf and Molnár, Vince}, booktitle = {MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems}, doi = {10.1145/3652620.3686251}, unique-id = {35600740}, abstract = {In the field of model-based systems engineering, there is an increasing demand for the application of formal methods. However, this requires expertise in formal methods, which cannot be expected from systems engineers. While several attempts have been made to bridge this gap, there are still open questions. (1) With the trend shifting towards ontological languages, systems are modeled as classes of 4D occurrences, rather than a 3D system evolving with time, which hinders the application of state-of-the-art model checking algorithms. (2) Ontological reasoning cannot handle the state space explosion problem, and can even make it harder for verifiers to operate efficiently. (3) When operationalizing ontological languages, we need to validate the conformance of the two semantics, even in the presence of optimizations. (4) On top of all, these challenges must be solved for every new engineering language, version, or variant. In this paper, we propose a new approach to address the aforementioned challenges. To validate its feasibility, we present a prototype tool and evaluate it on a SysML model.}, year = {2024}, pages = {311-317}, orcid-numbers = {Marussy, Kristóf/0000-0002-9135-8256; Molnár, Vince/0000-0002-8204-7595} } @inproceedings{MTMT:34895397, title = {The Common Requirement Modeling Language}, url = {https://m2.mtmt.hu/api/publication/34895397}, author = {Bouskela, Daniel and Buffoni, Lena and Jardin, Audrey and Molnair, Vince and Pop, Adrian and Zavada, Ármin}, booktitle = {Proceedings of the 15th International Modelica Conference 2023, Aachen, October 9-11}, doi = {10.3384/ecp204497}, unique-id = {34895397}, abstract = {CRML (the Common Requirement Modeling Language) is a new language for the formal expression of requirements. The ambition is to release the language as an open standard integrated into the open source modeling and simulation tool OpenModelica and interoperable with the open systems engineering standard SysMLv2. CRML allows to express requirements as multidisciplinary spatiotemporal constraints that can be verified against system design by co-simulating requirements models with behavioral models. Particular attention is paid to the following aspects. The requirements models must be easily legible and sharable between disciplines and stakeholders and must capture realistic constraints on the system, including time-dependent constraints with probabilistic criteria, in recognition of the fact that no constraint can be fulfilled at any time at any cost. The theoretical foundation of the language lies on 4-valued Boolean algebra, set theory and function theory. The coupling of the requirements models to the behavioral models is obtained through the specification of bindings, the automatic generation of Modelica code from the CRML model and use of the FMI and SSP standards. CRML and the proposed methodology is compatible with SysMLv2, forming a comprehensive work-flow and tool-chain encompassing requirement analysis, system design and V&V. The final objective is to facilitate the demonstration of correctness of system behavior against assumptions and requirements by building a workflow around Model-Driven Engineering and Open Standards for automating the creation of verification simulators.}, year = {2023}, pages = {497-510}, orcid-numbers = {Zavada, Ármin/0000-0001-7424-8410} }