Prototyping the semantics of a DSL using ASF+SDF: link to formal verification of DSL models

S. Andova, M.G.J. Brand, van den, L.J.P. Engelen

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    1 Downloads (Pure)

    Samenvatting

    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.
    Originele taal-2Engels
    TitelProceedings Second International Workshop on Algebraic Methods in Model-based Software Engineering (AMMSE'11, Zurich, Switzerland, June 30, 2011)
    RedacteurenF. Durán, V. Rusu
    UitgeverijEPTCS
    Pagina's65-79
    DOI's
    StatusGepubliceerd - 2011

    Publicatie series

    NaamElectronic Proceedings in Theoretical Computer Science
    Volume56
    ISSN van geprinte versie2075-2180

    Vingerafdruk

    Duik in de onderzoeksthema's van 'Prototyping the semantics of a DSL using ASF+SDF: link to formal verification of DSL models'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit