Software & Systems Modeling

, Volume 16, Issue 2, pp 357–392 | Cite as

Formal validation of domain-specific languages with derived features and well-formedness constraints

  • Oszkár Semeráth
  • Ágnes Barta
  • Ákos Horváth
  • Zoltán Szatmári
  • Dániel Varró
Special Section Paper

Abstract

Despite the wide range of existing tool support, constructing a design environment for a complex domain-specific language (DSL) is still a tedious task as the large number of derived features and well-formedness constraints complementing the domain metamodel necessitate special handling. Such derived features and constraints are frequently defined by declarative techniques (such graph patterns or OCL invariants). However, for complex domains, derived features and constraints can easily be formalized incorrectly resulting in inconsistent, incomplete or ambiguous DSL specifications. To detect such issues, we propose an automated mapping of EMF metamodels enriched with derived features and well-formedness constraints captured as graph queries in EMF-IncQuery or (a subset of) OCL invariants into an effectively propositional fragment of first-order logic which can be efficiently analyzed by back-end reasoners. On the conceptual level, the main added value of our encoding is (1) to transform graph patterns of the EMF-IncQuery framework into FOL and (2) to introduce approximations for complex language features (e.g., transitive closure or multiplicities) which are not expressible in FOL. On the practical level, we identify and address relevant challenges and scenarios for systematically validating DSL specifications. Our approach is supported by a tool, and it will be illustrated on analyzing a DSL in the avionics domain. We also present initial performance experiments for the validation using Z3 and Alloy as back-end reasoners.

Keywords

Language validation Derived features Partial snapshots Model queries SMT solvers 

Notes

Acknowledgments

This work was motivated by the FP7 ARTEMIS CONCERTO (ART-2012-333053) project, partially supported by the CERTIMOT (Design and Analysis Techniques for Certifiable Model Transformations, ERC_HU-09-01-2010-0003) project, the TÁMOP (4.2.2.C-11/1/KONV-2012-0001) project, a collaborative project with Embraer, the ARTEMIS JU and the Hungarian National Research, Development and Innovation Fund in the frame of the R5-COP (Reconfigurable ROS-based Resilient Reasoning Robotic Cooperating Systems) project.

References

  1. 1.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to Alloy. Softw. Syst. Model. 9(1), 69–86 (2010)CrossRefGoogle Scholar
  2. 2.
    Antkiewicz, M., Bak, K., Murashkin, A., Olaechea, R., Liang, J., Czarnecki, K.: Clafer tools for product line engineering. In: SPLC, Tokyo, Japan (2013)Google Scholar
  3. 3.
    ARINC—Aeronautical Radio, Incorporated: A653—Avionics Application Software Standard Interface. http://www.aviation-ia.com/standards
  4. 4.
    AUTOSAR Consortium: The AUTOSAR Standard (2013). http://www.autosar.org/
  5. 5.
    Bak, K., Czarnecki, K., Wasowski, A.: Feature and meta-models in clafer: mixed, specialized, and coupled. In: 3rd International Conference on Software Language Engineering. Eindhoven, The Netherlands (2010). doi: 10.1007/978-3-642-19440-5_7
  6. 6.
    Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: Proceedings of the VERIFY, Workshop at Federated Logic Conferences (FLoC), Copenhagen, Denmark (2002)Google Scholar
  7. 7.
    Bergmann, G., Horváth, Á., Ráth, I., Varró, D., Balogh, A., Balogh, Z., Ökrös, A.: Incremental evaluation of model queries over EMF models. In: MODELS’10, LNCS, vol. 6395. Springer (2010)Google Scholar
  8. 8.
    Bergmann, G., Ujhelyi, Z., Ráth, I., Varró, D.: A graph query language for EMF models. In: Cabot, J., Visser, E. (eds.) Fourth International Conference on Theory and Practice of Model Transformations, LNCS, vol. 6707, pp. 167–182. Springer (2011)Google Scholar
  9. 9.
    Bergmann, G.: Translating OCL to graph patterns. In: ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems, MODELS 2014. Springer, Valencia (2014)Google Scholar
  10. 10.
    Brucker, A.D., Wolff, B.: The HOL–OCL tool (2007). http://www.brucker.ch/
  11. 11.
    Büttner, F., Cabot, J.: Lightweight string reasoning for OCL. In: Vallecillo, A., Tolvanen, J.P., Kindler, E., Störrle, H., Kolovos, D.S. (eds.) Modelling Foundations and Applications—8th European Conference, ECMFA 2012, Lyngby, Denmark, July 2–5, 2012. Proceedings, LNCS, vol. 7349, pp. 244–258. Springer (2012)Google Scholar
  12. 12.
    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, ICFEM’12, pp. 198–213. LNCS 7635. Springer (2012)Google Scholar
  13. 13.
    Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ‘off-the-shelf’ SMT solvers. In: Proceedings of the 15th International Conference on MODELS, LNCS, vol. 7590 (2012)Google Scholar
  14. 14.
    Cabot, J., Clarisó, R., Riera, D.: UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE’07), pp. 547–548. ACM, New York (2007). doi: 10.1145/1321631.1321737
  15. 15.
    Cabot, J., Clariso, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: Software Testing Verification and Validation Workshop, 2008. ICSTW’08. IEEE International Conference on, pp. 73–80 (2008). doi: 10.1109/ICSTW.2008.54
  16. 16.
    Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: A UML/OCL framework for the analysis of graph transformation rules. Softw. Syst. Model. 9(3), 335–357 (2010)CrossRefGoogle Scholar
  17. 17.
    Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)CrossRefGoogle Scholar
  18. 18.
  19. 19.
    Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24 (2009)Google Scholar
  20. 20.
    Clavel, M., Egea, M.: The ITP/OCL tool (2008). http://maude.sip.ucm.es/itp/ocl/
  21. 21.
    Cunha, A., Garis, A., Riesco, D.: Translating between alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 5–25 (2013)Google Scholar
  22. 22.
    Dania, C., Clavel, M.: OCL2FOL+: coping with undefinedness. In: Cabot, J., Gogolla, M., Ráth, I., Willink, E.D. (eds.) OCL@MoDELS, CEUR Workshop Proceedings, vol. 1092, pp. 53–62. CEUR-WS.org (2013). http://dblp.uni-trier.de/db/conf/models/ocl2013.html#DaniaC13
  23. 23.
    De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 337–340. Springer (2008)Google Scholar
  24. 24.
    Famelis, M., Salay, R., Chechik, M.: Partial models: towards modeling and reasoning with uncertainty. In: Proceedings of the 34th International Conference on Software Engineering, ICSE’12, pp. 573–583. IEEE Press, Piscataway (2012). http://dl.acm.org/citation.cfm?id=2337223.2337290
  25. 25.
    Ge, Y., Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, LNCS, vol. 5643, pp. 306–320. Springer, Berlin (2009). doi: 10.1007/978-3-642-02658-4_25
  26. 26.
    Gogolla, M., Bohling, J., Richters, M.: Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4(4), 386–398 (2005)CrossRefGoogle Scholar
  27. 27.
    Grönniger, H., Ringert, J.O., Rumpe, B.: System model-based definition of modeling language semantics. In: Formal Techniques for Distributed Systems, LNCS, vol. 5522, pp. 152–166. Springer (2009)Google Scholar
  28. 28.
    Horváth, Á., Hegedüs, Á., Búr, M., Varró, D., Starr, R.R., Mirachi, S.: Hardware–software allocation specification of ima systems for early simulation. In: Digital Avionics Systems Conference (DASC). IEEE, IEEE, Colorado Springs, Colorado, US (2014)Google Scholar
  29. 29.
    Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Proceedings of the 14th International Conference on MODELS, LNCS, vol. 6981, pp. 653–667 (2011)Google Scholar
  30. 30.
    Jackson, E.K., Schulte, W., Bjørner, N.: Detecting specification errors in declarative languages with constraints. In: Proceedings of the 15th International Conference on MODELS, LNCS, vol. 7590, pp. 399–414 (2012)Google Scholar
  31. 31.
    Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002). doi: 10.1145/505145.505149 CrossRefGoogle Scholar
  32. 32.
    Khurshid, S., Marinov, D.: TestEra: specification-based testing of Java programs using SAT. Autom. Softw. Eng. 11(4), 403–434 (2004). doi: 10.1023/B:AUSE.0000038938.10589.b9 CrossRefGoogle Scholar
  33. 33.
    Kuhlmann, M., Gogolla, M.: From UML and OCL to Relational Logic and Back. Lecture Notes in Computer Science, vol. 7590. Springer, Berlin (2012). doi: 10.1007/978-3-642-33666-9_27
  34. 34.
    Kuhlmann, M., Gogolla, M.: Strengthening SAT-based validation of UML/OCL models by representing collections as relations. In: European Conference on Modelling Foundations and Applications, LNCS, vol. 7349, pp. 32–48 (2012)Google Scholar
  35. 35.
    Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into use. In: TOOLS’11—Objects, Models, Components and Patterns, LNCS, vol. 6705, pp. 290–306 (2011)Google Scholar
  36. 36.
    Liang, J.: Solving Clafer Models with Choco (GSDLab-TR 2012-12-30) (2012)Google Scholar
  37. 37.
    Lucio, L., Barroca, B., Amaral, V.: A technique for automatic validation of model transformations. In: Proceedings of the 13th International Conference on MODELS, LNCS, vol. 6394, pp. 136–150 (2010)Google Scholar
  38. 38.
    Mathworks: Matlab Simulink—Simulation and Model-Based Design. http://www.mathworks.com/products/simulink/
  39. 39.
  40. 40.
    Micskei, Z., Szatmári, Z., Oláh, J., Majzik, I.: A concept for testing robustness and safety of the context-aware behaviour of autonomous systems. In: Jezic, G., Kusek, M., Nguyen, N.T., Howlett, R., Jain, L. (eds.) Agent and Multi-Agent Systems. Technologies and Applications, LNCS, vol. 7327, pp. 504–513. Springer, Berlin (2012). doi: 10.1007/978-3-642-30947-2_55
  41. 41.
    Olaechea, R., Stewart, S., Czarnecki, K., Rayside, D.: Modeling and multi-objective optimization of quality attributes in variability-rich software. In: International Workshop on Non-functional System Properties in Domain Specific Modeling Languages. Innsbruck, Austria (2012)Google Scholar
  42. 42.
    Oszkár Semeráth: Validation of Domain Specific Languages. Technical Report (2013). https://incquery.net/publications/dslvalid
  43. 43.
    Piskac, R., de Moura, L., Bjorner, N.: Deciding effectively propositional logic with equality. Microsoft Research, MSR-TR-2008-181 Technical Report (2008)Google Scholar
  44. 44.
    Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: finite reasoning on UML/OCL conceptual schemas. Data Knowl. Eng. 73, 1–22 (2012)CrossRefGoogle Scholar
  45. 45.
    R3-cop (resilient reasoning robotic co-operative systems). ARTEMIS project no 100233. http://www.r3-cop.eu/
  46. 46.
    Ráth, I., Hegedüs, A., Varró, D.: Derived features for EMF by integrating advanced model queries. In: Vallecillo, A., Tolvanen, J.P., Kindler, E., Störrle, H., Kolovos, D. (eds.) Modelling Foundations and Applications, LNCS, vol. 7349, pp. 102–117. Springer, Berlin (2012). doi: 10.1007/978-3-642-31491-9_10
  47. 47.
    RTCA, S.C.: DO-178C, Software Considerations in Airborne Systems and Equipment Certification (2011)Google Scholar
  48. 48.
    SAE—Radio Technical Commission for Aeronautic: Architecture Analysis and Design Language (AADL) v2, AS-5506A, SAE International (2009)Google Scholar
  49. 49.
    Salay, R., Famelis, M., Chechik, M.: Language independent refinement using partial modeling. In: de Lara, J., Zisman, A. (eds.) Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, vol. 7212, pp. 224–239. Springer, Berlin (2012). doi: 10.1007/978-3-642-28872-2_16
  50. 50.
    Semeráth, O., Horváth, Á., Varró, D.: Validation of derived features and well-formedness constraints in DSLs—by mapping graph queries to an SMT-solver. In: MODELS—Proceedings of 16th International Conference, MODELS 2013, Miami, FL, USA, September 29–October 4, 2013, pp. 538–554 (2013)Google Scholar
  51. 51.
    Sen, S., Mottu, J.M., Tisi, M., Cabot, J.: Using models of partial knowledge to test model transformations. In: 5th International Conference on Theory and Practice of Model Transformations, LNCS, vol. 7307, pp. 24–39 (2012)Google Scholar
  52. 52.
    Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and back again. In: MoDeVVa ’09: Proceedings of the 6th International Workshop on Model-Driven Engineering, Verification and Validation, pp. 1–10. ACM (2009)Google Scholar
  53. 53.
    Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using boolean satisfiability. In: Design, Automation and Test in Europe (DATE’10), pp. 1341–1344. IEEE (2010)Google Scholar
  54. 54.
    The Eclipse Project: Eclipse Modeling Framework. http://www.eclipse.org/emf
  55. 55.
    The Eclipse Project: Zest. http://www.eclipse.org/gef/zest/
  56. 56.
    The Object Management Group: Object Constraint Language, v2.0 (2006). http://www.omg.org/spec/OCL/2.0/
  57. 57.
    Varró, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68(3), 214–234 (2007)MathSciNetCrossRefMATHGoogle Scholar
  58. 58.
    Willink, E.D.: An extensible OCL virtual machine and code generator. In: Proceedings of the 12th Workshop on OCL and Textual Modelling, pp. 13–18. ACM (2012)Google Scholar
  59. 59.
    Winkelmann, J., Taentzer, G., Ehrig, K., Küster, J.M.: Translation of restricted OCL constraints into graph constraints for generating meta model instances by graph grammars. ENTCS. In: Proceedings of the 5th International Workshop on Graph Transformation and Visual Modeling Techniques vol. 211, pp. 159–170 (2008). doi: 10.1016/j.entcs.2008.04.038
  60. 60.

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  1. 1.Department of Measurement and Information SystemsBudapest University of Technology and EconomicsBudapestHungary

Personalised recommendations