The STUDIA UNIVERSITATIS BABEŞ-BOLYAI issue article summary

The summary of the selected article appears at the bottom of the page. In order to get back to the contents of the issue this article belongs to you have to access the link from the title. In order to see all the articles of the archive which have as author/co-author one of the authors mentioned below, you have to access the link from the author's name.

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.