Alloy Community

User login

A Lightweight Approach for Defining the Formal Semantics of a Modeling Language

Authors: 
Pierre Kelsen & Qin Ma
Publication Venue: 
Model Driven Engineering Languages and Systems (MODELS) 2008
When Published: 
Sep 22 2008

To define the formal semantics of a modeling language, one
normally starts from the abstract syntax and then defines the static se-
mantics and dynamic semantics. Having a formal semantics is important
for reasoning about the language but also for building tools for the lan-
guage. In this paper we propose a novel approach for this task based
on the Alloy language. With the help of a concrete example language,
we contrast this approach with traditional methods based on formal lan-
guages, type checking, meta-modeling and operational semantics. Al-
though both Alloy and traditional techniques yield a formal semantics of
the language, the Alloy-based approach has two key advantages: a uni-
form notation, and immediate automatic analyzability using the Alloy
analyzer. Together with the simplicity of Alloy, our approach offers the
prospect of making formal definitions easier, hopefully paving the way
for a wider adoption of formal techniques in the definition of modeling
languages.



Attachment


Size
languagesemantics.pdf623.26 KB

Syndicate content  

The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.

Theme originally designed by Chris Herberte