%0 Report %1 kelsen_08_formal %A Kelsen, Pierre %A Ma, Qin %D 2008 %K 2008 _hardcopy semantics alloy %P 1--37 %T A Formal Definition of the EP Language %U http://democles.lassy.uni.lu/documentation/TR_LASSY_08_03.pdf %X The purpose of this paper is two-fold: rst, to give a formal semantics to a declarative executable modeling language called EP; second, to introduce a new approach for dening the formal semantics of a modeling language and to compare it, in the case of the EP language, with traditional approaches for dening the formal semantics of a modeling language. To define the formal semantics of a modeling language, one normally starts from the abstract syntax and then denes the static semantics and dynamic semantics. The availability of a formal semantics is important for reasoning about the language but also for building tools for the language. In this paper we propose the Alloy language as a unied notation for this task. For the concrete example of the EP language, we contrast the Alloy approach with traditional methods based on formal languages, type checking, meta-modeling and operational semantics. Although both Alloy and traditional techniques yield a formal semantics of the language, the Alloy-based approach has two key advantages: a uniform notation, and immediate automatic analyzability using the Alloy analyzer. Together with the simplicity of Alloy, our approach oers the prospect of making formal denitions easier, hopefully paving the way for a wider adoption of formal techniques in the definition of modeling languages.

@techreport{kelsen_08_formal, abstract = {The purpose of this paper is two-fold: rst, to give a formal semantics to a declarative executable modeling language called EP; second, to introduce a new approach for dening the formal semantics of a modeling language and to compare it, in the case of the EP language, with traditional approaches for dening the formal semantics of a modeling language. To define the formal semantics of a modeling language, one normally starts from the abstract syntax and then denes the static semantics and dynamic semantics. The availability of a formal semantics is important for reasoning about the language but also for building tools for the language. In this paper we propose the Alloy language as a unied notation for this task. For the concrete example of the EP language, we contrast the Alloy approach with traditional methods based on formal languages, type checking, meta-modeling and operational semantics. Although both Alloy and traditional techniques yield a formal semantics of the language, the Alloy-based approach has two key advantages: a uniform notation, and immediate automatic analyzability using the Alloy analyzer. Together with the simplicity of Alloy, our approach oers the prospect of making formal denitions easier, hopefully paving the way for a wider adoption of formal techniques in the definition of modeling languages.}, added-at = {2009-02-11T22:18:28.000+0100}, author = {Kelsen, Pierre and Ma, Qin}, biburl = {https://www.bibsonomy.org/bibtex/24be018faa5e8b2fb7fd0fb3ab8c5547d/leonardo}, citeulike-article-id = {3799179}, howpublished = {TR-LASSY-08-03}, institution = {Laboratory for Advanced Software Systems, University of Luxembourg}, interhash = {650ec85d04ff05c0770ce956f21f8c14}, intrahash = {4be018faa5e8b2fb7fd0fb3ab8c5547d}, keywords = {2008 _hardcopy semantics alloy}, month = May, pages = {1--37}, posted-at = {2008-12-17 01:43:27}, priority = {4}, timestamp = {2009-02-11T22:18:28.000+0100}, title = {A Formal Definition of the EP Language}, url = {http://democles.lassy.uni.lu/documentation/TR_LASSY_08_03.pdf}, year = 2008 }