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, the authors 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 them to apply existing tools for visualization and verification to models with little or no further effort.