Early Fault Detection in DSLs using SMT Solving and Automated Debugging
2013 (English) In: Software Engineering and Formal Methods: 11th International Conference, SEFM 2013, Madrid, Spain, September 2013 Proceedings / [ed] Robert Hierons, Mercedes G. Merayo & Mario Bravetti, Berlin: Springer Berlin/Heidelberg, 2013, Vol. 8137, p. 182-196Conference paper, Published paper (Refereed)
Abstract [en]
In the context of Domain Specic Languages (DSLs), westudy ways to detect faults early in the software development cycle. Wepropose techniques that validate a wide range of properties, classiedinto basic and advanced. Basic validation includes syntax checking, reference checking and type checking. Advanced validation concerns domainspecic properties related to the semantics of the DSL. For verication,we mechanically translate the DSL instance and the advanced propertiesinto Satisability Modulo Theory (SMT) problems, and solve these problems using an SMT solver. For user feedback, we extend the vericationwith automated debugging, which pinpoints the causes of the violatedproperties and traces them back to the syntactic constructs of the DSL.We illustrate this integration of techniques using an industrial case oncollision prevention for medical imaging equipment. © 2013 Springer-Verlag.
Place, publisher, year, edition, pages Berlin: Springer Berlin/Heidelberg, 2013. Vol. 8137, p. 182-196
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8137
Keywords [en]
Early Fault Detection, Formal Verification, Domain Specific Language (DSL), Satisfiability Module Theories (SMT), Automated Debugging, Delta Debugging
National Category
Computer and Information Sciences
Identifiers URN: urn:nbn:se:hh:diva-23496 DOI: 10.1007/978-3-642-40561-7_13 ISI: 000335436800013 Scopus ID: 2-s2.0-84885932542 ISBN: 978-3-642-40560-0 (print) OAI: oai:DiVA.org:hh-23496 DiVA, id: diva2:645868
Conference 11th International Conference on Software Engineering and Formal Methods, SEFM 2013, Madrid, Spain, 25-27 September, 2013
Funder ELLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications 2013-09-052013-09-052025-10-01 Bibliographically approved