Early fault detection in DSLs using SMT solving and automated debugging

S. Keshishzadeh, A.J. Mooij, M.R. Mousavi

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    1 Downloads (Pure)

    Abstract

    In the context of Domain Specific Languages (DSLs), we study ways to detect faults early in the software development cycle. We propose techniques that validate a wide range of properties, classified into basic and advanced. Basic validation includes syntax checking, reference checking and type checking. Advanced validation concerns domain specific properties related to the semantics of the DSL. For verification, we mechanically translate the DSL instance and the advanced properties into Satisfiability Modulo Theory (SMT) problems, and solve these problems using an SMT solver. For user feedback, we extend the verification with automated debugging, which pinpoints the causes of the violated properties and traces them back to the syntactic constructs of the DSL. We illustrate this integration of techniques using an industrial case on collision prevention for medical imaging equipment. Keywords: Early Fault Detection; Formal Verification; Domain Specific Language (DSL); Satisfiability Modulo Theories (SMT); Delta Debugging
    Original languageEnglish
    Title of host publicationSoftware Engineering and Formal Methods (11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings)
    EditorsR.M. Hierons, M.G. Merayo, M. Bravetti
    Place of PublicationBerlin
    PublisherSpringer
    Pages182-196
    ISBN (Print)978-3-642-40560-0
    DOIs
    Publication statusPublished - 2013
    Event11th International Conference on Software Engineering and Formal Methods (SEFM 2013), September 25-27, 2013, Madrid, Spain - Madrid, Spain
    Duration: 25 Sept 201327 Sept 2013
    http://antares.sip.ucm.es/sefm2013/

    Publication series

    NameLecture Notes in Computer Science
    Volume8137
    ISSN (Print)0302-9743

    Conference

    Conference11th International Conference on Software Engineering and Formal Methods (SEFM 2013), September 25-27, 2013, Madrid, Spain
    Abbreviated titleSEFM 2013
    Country/TerritorySpain
    CityMadrid
    Period25/09/1327/09/13
    Internet address

    Fingerprint

    Dive into the research topics of 'Early fault detection in DSLs using SMT solving and automated debugging'. Together they form a unique fingerprint.

    Cite this