R. Ahmadi, E. Posse, and J. Dingel, Slicing UML-based Models of Real-time Embedded Systems, Int. Conf. Model Driven Engineering Languages and Systems, pp.346-356, 2018.

T. Ali, M. Nauman, and M. Alam, An Accessible Formal Specification of the UML and OCL Meta-Model in Isabelle/HOL, 2007.

M. Conf and . Ieee,

K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, UML2Alloy: A challenging model transformation, Int. Conf. Model Driven Engineering Languages and Systems, pp.436-450, 2007.

K. Anastasakis, B. Bordbar, G. Georg, and I. Ray, On challenges of model transformation from UML to Alloy. Software & Systems Modeling, vol.9, pp.69-86, 2008.

A. Artale, D. Calvanese, and A. Ibánez-garc?a, Checking full satisfiability of conceptual models, Int. Work. Description Logics, p.55, 2010.

V. Bertram, S. Maoz, J. O. Ringert, B. Rumpe, and . Michael-von-wenckstern, Component and Connector Views in Practice: An Experience Report, Int. Conf. Model Driven Engineering Languages and Systems, pp.167-177, 2017.

G. V. Bochmann, S. Haar, C. Jard, and G. Jourdan, Testing Systems Specified as Partial Order Input/Output Automata, Testing of Software and Communicating Systems, pp.169-183, 2008.

D. Achim, J. Brucker, B. Doser, and . Wolff, An MDA framework supporting OCL, Electronic Communications of the EASST, vol.5, 2007.

D. Achim, B. Brucker, and . Wolff, HOL-OCL: A Formal Proof Environment for uml/ocl, Fundamental Approaches to Software Engineering, pp.97-100, 2008.

H. Bruneliere, E. Burger, J. Cabot, and M. Wimmer, A Featurebased Survey of Model View Approaches. Software and Systems Modeling, vol.18, pp.1931-1952, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01891295

J. Cabot, R. Clarisó, and D. Riera, UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming, Int. Conf. Automated Software Engineering, pp.547-548, 2007.

M. Cadoli, D. Calvanese, G. D. Giacomo, and T. Mancini, Finite Model Reasoning on UML Class Diagrams Via Constraint Programming, Artificial Intelligence and Human-Oriented Computing, pp.36-47, 2007.

M. Clavel, M. Egea, and M. A. García-de-dios, Checking unsatisfiability for OCL constraints, Electronic Communications of the EASST, vol.24, 2010.

C. Dania and M. Clavel, OCL2FOL+: Coping with Undefinedness, OCL@ MoDELS, vol.1092, pp.53-62, 2013.

C. Dania and M. Clavel, OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints, Int. Conf. Model Driven Engineering Languages and Systems, pp.65-75, 2016.

T. A. Luca-de-alfaro and . Henzinger, Interface automata, SIGSOFT Software Engineering Notes, vol.26, pp.109-120, 2001.

R. De, N. , and R. Segala, A process algebraic view of input/output automata, Theoretical Computer Science, vol.138, pp.391-423, 1995.

, -J Meeting on the mathematical foundation of programing semantics

I. Dragomir, I. Ober, and C. Percebois, Contract-based modeling and verification of timed safety requirements within SysML. Software & Systems Modeling, vol.16, pp.587-624, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01567085

E. Dustin, J. Rashka, and J. Paul, Automated Software Testing: Introduction, Management, and Performance, 1999.

P. Feiler, D. Gluch, and J. Hudak, The Architecture Analysis & Design Language (AADL): An Introduction, 2006.

S. Fendrich and G. Lüttgen, A generalised theory of interface automata, component compatibility and error, Int. Conf. Integrated Formal Methods, pp.160-175, 2016.

A. Formica, Finite satisfiability of integrity constraints in object-oriented database schemas, Transactions on Knowledge and Data Engineering, vol.14, pp.123-139, 2002.

A. Formica, Satisfiability of object-oriented database constraints with set and bag attributes, Information Systems, vol.28, issue.3, pp.213-224, 2003.

/. Doi,

M. Gogolla, J. Bohling, and M. Richters, Validating UML and OCL models in USE by automatic snapshot generation, Software & Systems Modeling, vol.4, pp.386-398, 2005.

M. Gogolla, F. Büttner, and M. Richters, USE: A UML-based specification environment for validating UML and OCL, Science of Computer Programming, vol.69, pp.27-34, 2007.

M. Gogolla, L. Hamann, and M. Kuhlmann, Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases, pp.38-54, 2010.

A. Carlos, F. González, R. Büttner, J. Clarisó, and . Cabot, EMFtoCSP: A tool for the lightweight verification of EMF models, Int. Work. Formal Methods in Software Engineering: Rigorous and Agile Approaches, pp.44-50, 2012.

A. Carlos, J. González, and . Cabot, Formal verification of static software models in MDE: A systematic review, Information and Software Technology, vol.56, pp.821-838, 2014.

. Iso/pas, Automation systems and integration -Object-Process Methodology, 2015.

. Itu, Formal semantics of message sequence charts. Recommendation Z, p.120, 1998.

B. Annex, International Telecommunication Union

, Message Sequence Chart (MSC). Recommendation Z.120. International Telecommunication Union, 2011.

, Specification and Description Language -Overview of SDL-2010. Recommendation Z.100. International Telecommunication Union, 2019.

K. Dilsun, N. Kaynar, R. Lynch, F. Segala, and . Vaandrager, The Theory of Timed I/O Automata, 2010.

T. Kehrer, G. Taentzer, M. Rindt, and U. Kelter, Automatically deriving the specification of model editing operations from meta-models, Int. Conf. Theory and Practice of Model Transformations, pp.173-188, 2016.

M. Kuhlmann and M. Gogolla, From UML and OCL to relational logic and back, Int. Conf. Model Driven Engineering Languages and Systems, pp.415-431, 2012.

U. Kim-g-larsen, A. Nyman, and . Wasowski, Modal I/O Automata for Interface and Product Line Theories, Programming Languages and Systems, pp.64-79, 2007.

G. Gurvan-le, Modeling requirements should be language agnostic! Example of a formal definition of simple Behavioral Decomposition Models, Int. Conf. Model-Driven Engineering and Software Development, pp.555-562, 2016.

M. Lenzerini and P. Nobili, On the satisfiability of dependency constraints in entity-relationship schemata, Information Systems, vol.15, pp.453-461, 1990.

A. Nancy, . Lynch, and . Mark-r-tuttle, An Introduction to Input/Output Automata, CWI Quaterly, vol.2, issue.3, pp.219-246, 1989.

S. Maoz, J. O. Ringert, and B. Rumpe, Verifying component and connector models against crosscutting structural views, Int. Conf. Software Engineering, pp.95-105, 2014.

A. Maraee and M. Balaban, Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets, Eur. Conf. Model Driven Architecture-Foundations and Applications, pp.17-31, 2007.

R. Marcano and . Levy, Using B formal specifications for analysis and verification of UML/OCL models, Work. consistency problems in UML-based software development. Citeseer, pp.91-105, 2002.

. Omg, OMG® Unified Modeling Language® (OMG UML®), 2017.

. Omg, OMG Systems Modeling Language (OMG SysML TM ). Standard. Object Management Group (OMG), 2019.

C. Pietsch, M. Ohrndorf, U. Kelter, and T. Kehrer, Incrementally slicing editable submodels, Int. Conf. Automated Software Engineering, pp.913-918, 2017.

A. Queralt, A. Artale, D. Calvanese, and E. Teniente, OCL-Lite: Finite reasoning on UML/OCL conceptual schemas, Data & Knowledge Engineering, vol.73, pp.1-22, 2012.

A. Queralt, G. Rull, E. Teniente, C. Farré, and T. Urpí, AuRUS: Automated Reasoning on UML/OCL Schemas, Conceptual Modeling, 2010.

H. Springer-berlin, , pp.438-444

A. Queralt and E. Teniente, Reasoning on UML Class Diagrams with OCL Constraints, pp.497-512, 2006.

L. Ab and . Rahim, Mapping from OCL/UML metamodel to PVS metamodel, Int. Symp. Information Technology. IEEE, 2008.

M. Rindt, T. Kehrer, and U. Kelter, Automatic Generation of Consistency-Preserving Edit Operations for MDE Tools, Demos@MoDELS, 2014.

D. Roe, K. Broda, and A. Russo, Mapping UML models incorporating OCL constraints into Object-Z. Imperial College of Science, Technology and Medicine, 2003.

P. Roques, MBSE with the ARCADIA Method and the Capella Tool, Eur. Cong. Embedded Real Time Software and Systems, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01258014

G. Rull, C. Farré, E. Teniente, and T. Urpí, Providing explanations for database schema validation, Int. Conf. Database and Expert Systems Applications, pp.660-667, 2008.

M. Schrefl and M. Stumptner, Behavior-consistent specialization of object life cycles, Transactions on Software Engineering and Methodology, vol.11, pp.92-148, 2002.

M. Soeken, R. Wille, and R. Drechsler, Encoding OCL data types for SAT-based verification of UML/OCL models, Int. Conf. Tests and Proofs, pp.152-170, 2011.

M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla, and R. Drechsler, Verifying UML/OCL models using Boolean satisfiability, Conf. Design, Automation and Test in Europe. European Design and Automation Association, pp.1341-1344, 2010.

M. Szlenk, Formal semantics and reasoning about uml class diagram, Int. Conf. Dependability of Computer Systems, pp.51-59, 2006.

M. Weckesser, M. Lochau, M. Ries, and A. Schürr, Towards complete consistency checks of clafer models, In Int. Work. Feature-Oriented Software Development. ACM, pp.11-20, 2017.

M. Weckesser, M. Lochau, M. Ries, and A. Schürr, Mathematical Programming for Anomaly Analysis of Clafer Models, Int. Conf. Model Driven Engineering Languages and Systems, pp.34-44, 2018.

R. Wille, M. Soeken, and R. Drechsler, Debugging of inconsistent UML/OCL models, Conf. Design, Automation and Test in Europe. EDA Consortium, pp.1078-1083, 2012.

H. Wu, Finding achievable features and constraint conflicts for inconsistent metamodels, Eur. Conf. Modelling Foundations and Applications, pp.179-196, 2017.

H. Wu, MaxUSE: a tool for finding achievable constraints and conflicts for inconsistent UML class diagrams, Int. Conf. Integrated Formal Methods, pp.348-356, 2017.

F. Zhang, Y. Zhao, D. Sanán, Y. Liu, A. Tiu et al., Compositional Reasoning for Shared-Variable Concurrent Programs, Int. Symp. Formal Methods, pp.523-541, 2018.