Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models
A formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the sp...
Main Authors: | , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2011-06-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1107.0067v1 |
id |
doaj-b3407486dcce45aea35b3286e92c2d99 |
---|---|
record_format |
Article |
spelling |
doaj-b3407486dcce45aea35b3286e92c2d992020-11-24T21:13:26ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-06-0156Proc. AMMSE 2011657910.4204/EPTCS.56.5Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL ModelsSuzana AndovaMark van den BrandLuc EngelenA formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the specification of systems consisting of concurrent, communicating objects. Using this prototype, models specified in the DSL can be transformed to labeled transition systems (LTS). This approach of transforming models to LTSs allows us to apply existing tools for visualization and verification to models with little or no further effort. The prototype is implemented using the ASF+SDF Meta-Environment, an IDE for the algebraic specification language ASF+SDF, which offers efficient execution of the transformation as well as the ability to read models and produce LTSs without any additional pre or post processing. http://arxiv.org/pdf/1107.0067v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Suzana Andova Mark van den Brand Luc Engelen |
spellingShingle |
Suzana Andova Mark van den Brand Luc Engelen Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models Electronic Proceedings in Theoretical Computer Science |
author_facet |
Suzana Andova Mark van den Brand Luc Engelen |
author_sort |
Suzana Andova |
title |
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models |
title_short |
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models |
title_full |
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models |
title_fullStr |
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models |
title_full_unstemmed |
Prototyping the Semantics of a DSL using ASF+SDF: Link to Formal Verification of DSL Models |
title_sort |
prototyping the semantics of a dsl using asf+sdf: link to formal verification of dsl models |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2011-06-01 |
description |
A formal definition of the semantics of a domain-specific language (DSL) is a key prerequisite for the verification of the correctness of models specified using such a DSL and of transformations applied to these models. For this reason, we implemented a prototype of the semantics of a DSL for the specification of systems consisting of concurrent, communicating objects. Using this prototype, models specified in the DSL can be transformed to labeled transition systems (LTS). This approach of transforming models to LTSs allows us to apply existing tools for visualization and verification to models with little or no further effort. The prototype is implemented using the ASF+SDF Meta-Environment, an IDE for the algebraic specification language ASF+SDF, which offers efficient execution of the transformation as well as the ability to read models and produce LTSs without any additional pre or post processing. |
url |
http://arxiv.org/pdf/1107.0067v1 |
work_keys_str_mv |
AT suzanaandova prototypingthesemanticsofadslusingasfsdflinktoformalverificationofdslmodels AT markvandenbrand prototypingthesemanticsofadslusingasfsdflinktoformalverificationofdslmodels AT lucengelen prototypingthesemanticsofadslusingasfsdflinktoformalverificationofdslmodels |
_version_ |
1716749251161096192 |