Cited By
View all- Huisman MRubin J(2018)Software quality tools and techniques presented in FASE'17International Journal on Software Tools for Technology Transfer (STTT)10.5555/3288063.328808420:6(611-613)Online publication date: 1-Nov-2018
Slicing ATL model transformations for scalable deductive verification and fault localization
Authors: 
Zheng Cheng, Massimo TisiAuthors Info & Claims
Pages 645 - 663
Abstract
Model-driven engineering (MDE) is increasingly accepted in industry as an effective approach for managing the full life cycle of software development. In MDE, software models are manipulated, evolved and translated by model transformations (MT), up to code generation. Automatic deductive verification techniques have been proposed to guarantee that transformations satisfy correctness requirements (encoded as transformation contracts). However, to be transferable to industry, these techniques need to be scalable and provide the user with easily accessible feedback. In MT-specific languages like ATL, we are able to infer static trace information (i.e., mappings among types of generated elements and rules that potentially generate these types). In this paper, we show that this information can be used to decompose the MT contract and, for each sub-contract, slice the MT to the only rules that may be responsible for fulfilling it. Based on this contribution, we design a fault localization approach for MT, and a technique to significantly enhance scalability when verifying large MTs against a large number of contracts. We implement both these algorithms as extensions of the VeriATL verification system, and we show by experimentation that they increase its industry readiness.
References
[1]
Ab. Rahim, L., Whittle, J.: A survey of approaches for verifying model transformations. Softw. Syst. Model. 14(2), 1003---1028 (2015)
[2]
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447---466 (2010)
[3]
Aranega, V., Mottu, J., Etien, A., Dekeyser, J.: Traceability mechanism for error localization in model transformation. In: 4th International Conference on Software and Data Technologies, pp. 66---73. Sofia, Bulgaria (2009)
[4]
Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: 4th International Conference on Formal Methods for Components and Objects, pp. 364---387. Springer, Amsterdam, Netherlands (2006)
[5]
Berghofer, S., Nipkow, T.: Random testing in Isabelle/HOL. In: 2nd International Conference on Software Engineering and Formal Methods, pp. 230---239. IEEE, Beijing, China (2004)
[6]
Berry, G.: Synchronous design and verification of critical embedded systems using SCADE and Esterel. In: 12th International Workshop on Formal Methods for Industrial Critical Systems, pp. 2---2. Springer, Berlin, Germany (2008)
[7]
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions, 1st edn. Springer, Berlin (2010)
[8]
Briand, L.C.: Making model-driven verification practical and scalable--experiences and lessons learned. In: 4th International Conference on Model-Driven Engineering and Software Development. SCITEPRESS, Rome, Italy (2016)
[9]
Burgueño, L., Troya, J., Wimmer, M., Vallecillo, A.: Static fault localization in model transformations. IEEE Trans. Softw. Eng. 41(5), 490---506 (2015)
[10]
Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using `off-the-shelf' SMT solvers. In: 15th International Conference on Model Driven Engineering Languages and Systems, pp. 198---213. Springer, Innsbruck, Austria (2012)
[11]
Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL transformations using transformation models and model finders. In: 14th International Conference on Formal Engineering Methods, pp. 198---213. Springer, Kyoto, Japan (2012)
[12]
Calegari, D., Luna, C., Szasz, N., Tasistro, Á.: A type-theoretic framework for certified model transformations. In: 13th Brazilian Symposium on Formal Methods, pp. 112---127. Springer, Natal, Brazil (2011)
[13]
Cheng, Z., Monahan, R., Power, J.F.: A sound execution semantics for ATL via translation validation. In: 8th International Conference on Model Transformation, pp. 133---148. Springer, L'Aquila, Italy (2015)
[14]
Cheng, Z., Monahan, R., Power, J.F.: Formalised EMFTVM bytecode language for sound verification of model transformations. Softw. Syst. Model. (2016).
[15]
Cheng, Z., Tisi, M.: A deductive approach for fault localization in ATL model transformations. In: 20th International Conference on Fundamental Approaches to Software Engineering, pp. 300---317. Springer, Uppsala, Sweden (2017)
[16]
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. ACM SIGPLAN Not. 46(4), 53---64 (2011)
[17]
Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: 25th IEEE International Symposium on Software Reliability Engineering, pp. 34---44. IEEE, Naples, Italy (2014)
[18]
Cuadrado, J.S., Guerra, E., de Lara, J., Clarisó, R., Cabot, J.: Translating target to source constraints in model-to-model transformations. In: 20th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 12---22. IEEE, Austin, TX, USA (2017)
[19]
Filliâtre, J.C., Paskevich, A.: Why3--where programs meet provers. In: 22nd European Symposium on Programming, pp. 125---128. Springer, Rome, Italy (2013)
[20]
Harman, M., Binkley, D., Danicic, S.: Amorphous program slicing. J. Syst. Softw. 68(1), 45---64 (2003)
[21]
Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1---16:58 (2012)
[22]
Hidaka, S., Jouault, F., Tisi, M.: On additivity in transformation languages. In: 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems, pp. 23---33. IEEE, Austin, TX, USA (2017)
[23]
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576---580 (1969)
[24]
Howard, W.A.: The formulae-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479---490. Academic Press (1980)
[25]
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, Cambridge (2004)
[26]
Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Softw. Eng. 37(5), 649---678 (2011)
[27]
Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: a model transformation tool. Sci. Comput. Program. 72(1---2), 31---39 (2008)
[28]
Kehrer, T., Taentzer, G., Rindt, M., Kelter, U.: Automatically deriving the specification of model editing operations from meta-models. In: 9th International Conference on Model Transformation, pp. 173---188. Springer, Vienna, Austria (2016)
[29]
Lano, K., Clark, T., Kolahdouz-Rahimi, S.: A framework for model transformation verification. Form. Asp. Comput. 27(1), 193---235 (2014)
[30]
Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting. https://www.microsoft.com/en-us/research/publication/verification-condition-splitting/ (2008)
[31]
de Moura, L., BjØrner, N.: Z3: An efficient SMT solver. In: 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337---340. Springer, Budapest, Hungary (2008)
[32]
Oakes, B.J., Troya, J., Lúcio, L., Wimmer, M.: Fully verifying transformation contracts for declarative ATL. In: 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, pp. 256---265. IEEE, Ottawa, ON (2015)
[33]
Object Management Group: Unified modeling language (ver. 2.5). http://www.omg.org/spec/UML/2.5/ (2015)
[34]
Poernomo, I.: Proofs-as-model-transformations. In: 1st International Conference on Model Transformation, pp. 214---228. Springer, Zürich, Switzerland (2008)
[35]
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Int. J. Softw. Tools Technol. Transf. 7(2), 156---173 (2005)
[36]
Radke, H., Arendt, T., Becker, J.S., Habel, A., Taentzer, G.: Translating essential OCL invariants to nested graph constraints focusing on set operations. In: 8th International Conference on Graph Transformation, pp. 155---170. Springer, L'Aquila, Italy (2015)
[37]
Roychoudhury, A., Chandra, S.: Formula-based software debugging. Commun. ACM 59, 68---77 (2016)
[38]
Selim, G., Wang, S., Cordy, J., Dingel, J.: Model transformations for migrating legacy models: an industrial case study. In: 8th European Conference on Modelling Foundations and Applications, pp. 90---101. Springer, Lyngby, Denmark (2012)
[39]
Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework, 2nd edn. Pearson Education, London (2008)
[40]
Tip, F.: A survey of program slicing techniques. Tech. rep., Centrum Wiskunde & Informatica (1994)
[41]
Tisi, M., Perez, S.M., Choura, H.: Parallel execution of ATL transformation rules. In: 16th International Conference on Model-Driven Engineering Languages and Systems, pp. 656---672. Springer, Miami, FL, USA (2013)
[42]
Wagelaar, D.: Using ATL/EMFTVM for import/export of medical data. In: 2nd Software Development Automation Conference. Amsterdam, Netherlands (2014)
[43]
Weiser, M.: Program slicing. In: 5th International Conference on Software Engineering, pp. 439---449. IEEE, NJ, USA (1981)
[44]
Wong, W.E., Gao, R., Li, Y., Abreu, R., Wotawa, F.: A survey on software fault localization. IEEE Trans. Softw. Eng. Pre-Print 99, 1---41 (2016)
- Slicing ATL model transformations for scalable deductive verification and fault localization
Recommendations
Verification of ATL transformations using transformation models and model finders
ICFEM'12: Proceedings of the 14th international conference on Formal Engineering Methods: formal methods and software engineeringIn model-driven engineering, models constitute pivotal elements of the software to be built. If models are specified well, transformations can be employed for different purposes, e.g., to produce final code. However, it is important that models produced ...
Full contract verification for ATL using symbolic execution
The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the ...
Automated verification of model transformations based on visual contracts
Model-Driven Engineering promotes the use of models to conduct the different phases of the software development. In this way, models are transformed between different languages and notations until code is generated for the final application. Hence, the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Copyright © 2018 Springer-Verlag GmbH Germany, part of Springer Nature.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 November 2018
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
Cited By
View all- Huisman MRubin J(2018)Software quality tools and techniques presented in FASE'17International Journal on Software Tools for Technology Transfer (STTT)10.5555/3288063.328808420:6(611-613)Online publication date: 1-Nov-2018
View Options
View options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in