Formal verification of static software models in MDE: A systematic review
CA González, J Cabot - Information and Software Technology, 2014 - Elsevier
Abstract Context Model-driven Engineering (MDE) promotes the utilization of models as
primary artifacts in all software engineering activities. Therefore, mechanisms to ensure …
primary artifacts in all software engineering activities. Therefore, mechanisms to ensure …
[HTML][HTML] QMaxUSE: A new tool for verifying UML class diagrams and OCL invariants
H Wu - Science of Computer Programming, 2023 - Elsevier
Formal verification of a UML class diagram annotated with OCL constraints has been a long-
standing challenge in Model-driven Engineering. In the past decades, many tools and …
standing challenge in Model-driven Engineering. In the past decades, many tools and …
From UML and OCL to relational logic and back
M Kuhlmann, M Gogolla - … on model driven engineering languages and …, 2012 - Springer
Languages like UML and OCL are used to precisely model systems. Complex UML and
OCL models therefore represent a crucial part of model-driven development, as they …
OCL models therefore represent a crucial part of model-driven development, as they …
Practical constraint solving for generating system test data
The ability to generate test data is often a necessary prerequisite for automated software
testing. For the generated data to be fit for their intended purpose, the data usually have to …
testing. For the generated data to be fit for their intended purpose, the data usually have to …
Towards the automated generation of consistent, diverse, scalable and realistic graph models
Automated model generation can be highly beneficial for various application scenarios
including software tool certification, validation of cyber-physical systems or benchmarking …
including software tool certification, validation of cyber-physical systems or benchmarking …
Formal validation of domain-specific languages with derived features and well-formedness constraints
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 …
complex domain-specific language (DSL) is still a tedious task as the large number of …
OCL Rebuilt, From the Ground Up
The Object Constraint Language (OCL) serves the expression of complex conditions and
queries over UML-based models in an object-oriented style. We note that OCL's grounding …
queries over UML-based models in an object-oriented style. We note that OCL's grounding …
[PDF][PDF] QMaxUSE: A query-based verification tool for UML class diagrams with OCL invariants
H Wu - … Conference on Fundamental Approaches to Software …, 2022 - library.oapen.org
Verifying whether a UML class diagram annotated with Object Constraint Language (OCL)
constraints is consistent involves finding valid instances that provably meet its structural and …
constraints is consistent involves finding valid instances that provably meet its structural and …
Generating metamodel instances satisfying coverage criteria via SMT solving
H Wu - 2016 4th International Conference on Model-Driven …, 2016 - ieeexplore.ieee.org
One of the challenges for using metamodels in Model Driven Engineering is to automatically
generate metamodel instances. Each instance should satisfy many constraints defined by a …
generate metamodel instances. Each instance should satisfy many constraints defined by a …
OCLVerifer: Automated verification of OCL contracts in requirements models
P Yang, L Zhang, Q Li, X Gao, Y Yang - Science of Computer Programming, 2025 - Elsevier
Abstract Object Constraint Language (OCL) is one lightweight formal specification.
Integrated within the Unified Modeling Language (UML) standard, it serves as a cornerstone …
Integrated within the Unified Modeling Language (UML) standard, it serves as a cornerstone …