symbolic execution; graph transformation; test case generation; triple graph grammars; EMF henshin
Résumé :
[en] Symbolic execution is a well-studied technique for analysing
the behaviour of software components with applications to test case generation. We propose a framework for symbolically executing satellite control procedures and generating test cases based on graph transformation
techniques. A graph-based operational symbolic execution semantics is
defined and the executed procedure models are used for generating test
cases by performing model transformations. The approach is discussed
based on a prototype implementation using the Eclipse Modelling Framework (EMF), Henshin and ECLiPSe-CLP tool ecosystem.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
NACHTIGALL, Nico ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
BRAATZ, Benjamin ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
ENGEL, Thomas ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Langue du document :
Anglais
Titre :
Symbolic Execution of Satellite Control Procedures in Graph-Transformation-Based EMF Ecosystems
Date de publication/diffusion :
2013
Nom de la manifestation :
10th International Workshop on Model Driven Engineering, Verification and Validation
Anand, S., Pasareanu, C. S., Visser, W.: JPF-SE: A symbolic execution extension to java pathfinder. In: TACAS. pp. 134-138 (2007)
Arusoaie, A., Lucanu, D., Rusu, V.: A Generic Approach to Symbolic Execution. Tech. Rep. RR-8189, INRIA (Dec. 2012)
Cadar, C., Dunbar, D., Engler, D.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on Operating systems design and implementation. pp. 209-224. OSDI'08, USENIX Association, Berkeley, CA, USA (2008)
Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82-90 (Feb. 2013)
The Eclipse Foundation: Xtext (2013), http://www.eclipse.org/Xtext
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation, vol. EATCS Monographs in Theoretical Computer Science. Springer (2006)
Hermann, F., Gottmann, S., Nachtigall, N., Braatz, B., Morelli, G., Pierre, A., Engel, T.: On an Automated Translation of Satellite Procedures Using Triple Graph Grammars. In: Proc. ICMT'13, LNCS, vol. 7909, pp. 50-51. Springer (2013)
Schimpf, J., Shen, K.: Eclipse - from lp to clp. Theory and Practice of Logic Programming 12, 127-156 (2012)
Zurowska, K., Dingel, J.: Symbolic execution of UML-RT State Machines. In: Proc. of SAC'12. pp. 1292-1299. SAC'12, ACM (2012)
