Rezumat articol ediţie STUDIA UNIVERSITATIS BABEŞ-BOLYAI

În partea de jos este prezentat rezumatul articolului selectat. Pentru revenire la cuprinsul ediţiei din care face parte acest articol, se accesează linkul din titlu. Pentru vizualizarea tuturor articolelor din arhivă la care este autor/coautor unul din autorii de mai jos, se accesează linkul din numele autorului.

The Alf language was introduced as a simpler, textual definition of fUML executable models. The operational semantics of Alf is defined by mapping the Alf concrete syntax to the abstract syntax of fUML.The operational semantics of fUML is described in a semi-formal way, focusing on its implementation in Java. Our paper addresses two problems regarding this issue: i) semantic integration, namely semantics mappings should be defined using platform independent constructions, and ii) the correctness of the execution engine must be guaranteed. We propose an approach to give a formal definition of Alf in the K-semantic framework. Executable K-definitions will specify a reference virtual machine that can gain access to K`s tools for formal analysis and verification.

2010 Mathematics Subject Classification. 68N30, 68Q60.1998 CR Categories and Descriptors. D.2.4 [Software/Program Verification]: Subtopic - Validation; F.3.1 [Specifying and Verifying and Reasoning about Programs]: Subtopic - Logics of programs.

Key words and phrases. fUML, K-Framework, Formal Methods.This paper has been presented at the International Conference KEPT2013: Knowledge Engineering Principles and Techniques, organized by Babes-Bolyai University, Cluj-Napoca, July 5-7 2013.