Title
Early Fault Detection in DSLs using SMT Solving and Automated Debugging
Author
Keshishzadeh, S.
Mooij, A.J.
Reza Mousavi, M.
Publication year
2013
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.
Subject
Communication & Information
ESI - Embedded Systems Innovation
TS - Technical Sciences
High Tech Systems & Materials
Electronics
Industrial Innovation
Automated debugging
Delta debugging
Domain specific languages
DSL
Early Fault Detection
Fault detection
Formal logic
Formal Verification
Early fault detection
Formal verification
Medical imaging equipment
Satisfiability Modulo Theories
SMT
Software development cycles
Software engineering
Semantics
Syntactics
To reference this document use:
http://resolver.tudelft.nl/uuid:d8367c4a-4d76-4a9a-a2ea-e4a5656a6140
DOI
https://doi.org/10.1007/978-3-642-40561-7_13
TNO identifier
480755
ISBN
9783642405600
ISSN
0302-9743
Source
Proceedings of the 11th International Conference on Software Engineering and Formal Methods, SEFM 2013, 25 September 2013 through 27 September 2013, Madrid, 8137 LNCS, 182-196
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Document type
conference paper