Wu, Hao (2017) MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams. In: Integrated Formal Methods : Proceedings. Lecture Notes in Computer Science (10510). Springer, Cham, Switzerland, pp. 348-356. ISBN 978-3-319-66844-4

Preview

Download (403kB) | Preview

Abstract

In the context of Model Driven Engineering (MDE), the structure of a system is typically described by using a UML class diagram annotated with a set of Object Constraint Language (OCL) constraints. These constraints specify rules that are not expressible by using structural features. These constraints can be conflicting, resulting in inconsistencies. When this happens, the existing tools terminate and provide no information about which constraints are achievable and which ones cause conflicts. In this paper, we present MaxUSE, a tool for finding achievable OCL constraints and conflicts for inconsistent UML class diagrams. MaxUSE integrates the USE modeling tool with a satisfiability modulo theories (SMT) solver. It finds a set of achievable constraints based on their rankings by casting to a weighted MaxSMT problem and at the same time locates constraint conflicts. We use an example to demonstrate MaxUSE’s usage scenarios and discuss its usefulness to the community.

Item Type:	Book Section
Additional Information:	This paper was presented at 13th International Conference, IFM 2017 Turin, Italy, September 20–22, 2017.
Keywords:	Embedded systems; Encoding (symbols); Model-driven Engineering; Object Constraint Language; Satisfiability modulo Theories; Structural feature; UML class diagrams; Usage scenarios; Use-model; Formal methods
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	11977
Identification Number:	https://doi.org/10.1007/978-3-319-66845-1_23
Depositing User:	Hao Wu
Date Deposited:	03 Dec 2019 12:26
Publisher:	Springer
Refereed:	Yes
URI:	Publisher
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads