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

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)

Antkiewicz, M., Bak, K., Murashkin, A., Olaechea, R., Liang, J., Czarnecki, K.: Clafer tools for product line engineering. In: SPLC, Tokyo, Japan (2013)

ARINC—Aeronautical Radio, Incorporated: A653—Avionics Application Software Standard Interface. http://www.aviation-ia.com/standards

AUTOSAR Consortium: The AUTOSAR Standard (2013). http://www.autosar.org/

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

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)

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)

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)

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)

Brucker, A.D., Wolff, B.: The HOL–OCL tool (2007). http://www.brucker.ch/

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)

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)

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)

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

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

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)

Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)

Choco. http://www.emn.fr/z-info/choco-solverp

Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24 (2009)

Clavel, M., Egea, M.: The ITP/OCL tool (2008). http://maude.sip.ucm.es/itp/ocl/

Cunha, A., Garis, A., Riesco, D.: Translating between alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 5–25 (2013)

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

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)

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

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

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)

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)

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)

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)

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)

Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002). doi: 10.1145/505145.505149

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

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

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)

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)

Liang, J.: Solving Clafer Models with Choco (GSDLab-TR 2012-12-30) (2012)

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)

Mathworks: Matlab Simulink—Simulation and Model-Based Design. http://www.mathworks.com/products/simulink/

Microsoft Research: Pex. http://research.microsoft.com/projects/pex/

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

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)

Oszkár Semeráth: Validation of Domain Specific Languages. Technical Report (2013). https://incquery.net/publications/dslvalid

Piskac, R., de Moura, L., Bjorner, N.: Deciding effectively propositional logic with equality. Microsoft Research, MSR-TR-2008-181 Technical Report (2008)

Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: finite reasoning on UML/OCL conceptual schemas. Data Knowl. Eng. 73, 1–22 (2012)

R3-cop (resilient reasoning robotic co-operative systems). ARTEMIS project no 100233. http://www.r3-cop.eu/

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

RTCA, S.C.: DO-178C, Software Considerations in Airborne Systems and Equipment Certification (2011)

SAE—Radio Technical Commission for Aeronautic: Architecture Analysis and Design Language (AADL) v2, AS-5506A, SAE International (2009)

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

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)

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)

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)

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)

The Eclipse Project: Eclipse Modeling Framework. http://www.eclipse.org/emf

The Eclipse Project: Zest. http://www.eclipse.org/gef/zest/

The Object Management Group: Object Constraint Language, v2.0 (2006). http://www.omg.org/spec/OCL/2.0/

Varró, D., Balogh, A.: The model transformation language of the VIATRA2 framework. Sci. Comput. Program. 68(3), 214–234 (2007)

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)

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

yEd Graph Editor: yED. http://www.yworks.com/en/products_yed_about.html