Special Issue on the 18th IEEE International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS 2015); Guest Editor: Zoran StamenkovićNo Access

Analyzing Inconsistencies in UML/OCL Models

Nils Przigoda

Group for Computer Architecture, University of Bremen, 28359 Bremen, Germany

E-mail Address: [email protected]

Corresponding author.

Search for more papers by this author

Robert Wille

Institute for Integrated Circuits, Johannes Kepler University Linz, A-4040 Linz, Austria

Cyber-Physical Systems, DFKI GmbH, 28359 Bremen, Germany

Search for more papers by this author

, and

Rolf Drechsler

Group for Computer Architecture, University of Bremen, 28359 Bremen, Germany

Cyber-Physical Systems, DFKI GmbH, 28359 Bremen, Germany

Search for more papers by this author

https://doi.org/10.1142/S0218126616400211Cited by:20 (Source: Crossref)

Abstract

Modeling languages such as the unified modeling language (UML) or the systems modeling language (SysML) in combination with constraint languages such as the object constraint language (OCL) allows for an abstract description of a system prior to its implementation. But the resulting system models can be highly non-trivial and, hence, errors in the descriptions can easily arise. In particular, too strong restrictions leading to an inconsistent model are common. Motivated by this, researchers and engineers developed methods for the validation and verification of given formal models. However, while these methods are efficient to detect the existence of an inconsistency, the designer is usually left alone to identify the reasons for it. In this contribution, we propose an automatic method which efficiently determines reasons explaining the contradiction in an inconsistent UML/OCL model. For this purpose, all constraints causing the contradiction are comprehensibly analyzed. By this, the designer is aided during the debugging of his/her model.

Keywords:

References

1. J. Rumbaugh, I. Jacobson and G. Booch (eds.), The Unified Modeling Language reference manual (Addison-Wesley Longman Inc, Masachusetto, 1999). Google Scholar
2. G. Martin and W. Mller, UML for SOC Design, 1st edn. (Springer, The Netherlands, 2005). Crossref, Google Scholar
3. T. Weilkiens, Systems Engineering with SysML/UML:Modeling, Analysis, Design (Morgan Kaufmann, USA, 2007). Google Scholar
4. J. Warmer and A. Kleppe, The Object Constraint Language: Precise Modeling with UML (Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1999). Google Scholar
5. M. Gogolla, F. Büttner and M. Richters, USE: A UML-based specification environment for validating UML and OCL, Sci. Comput. Program. 69 (2007) 27–34. Crossref, Web of Science, Google Scholar
6. M. Gogolla, M. Kuhlmann and L. Hamann, Consistency, independence and consequences in UML and OCL models, Tests and Proof Series in Lecture Notes in Computer Science (Springer Berlin Heidelberg, Switzerland, 2009), pp. 90–104. Crossref, Google Scholar
7. M. Kyas, H. Fecher, F. S. de Boer, J. Jacob, J. Hooman, M. van der Zwaag, T. Arons and H. Kugler, Formalizing UML Models and OCL Constraints in PVS, Electronic Notes in Theoretical Computer Science 115 (2005) 39–47. Crossref, Google Scholar
8. A. D. Brucker and B. Wolff, A Proposal for a Formal OCL Semantics Isabelle/HOL, Theorem Proving in Higher Order Logics Ser. Lecture Notes in Computer Science (Springer, Hampton, VA, USA, 2002), pp. 99–114. Crossref, Google Scholar
9. B. Beckert, R. Hähnle and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach Ser. Lecture Notes in Artificial Intelligence (Springer, Verlog Berlin Heidelberg, Germany, 2007). Google Scholar
10. J. Cabot, R. Clarisó and D. Riera, Verification of UML/OCL Class Diagrams using Constraint Programming, 9–April 2008 IEEE Int. Conf. Softw. Test. Verif. Validation Workshop (2008). Google Scholar
11. T. Mancini, Finite satisfiability of UML class diagrams by constraint programming, Description Logics (ACM, NewYork, USA, 2007) 547–548. Google Scholar
12. H. Malgouyres and G. Motet, A UML model consistency verification approach based on meta-modeling formalization, Symp. Appl. Comput (2006). Google Scholar
13. D. Berardi, D. Calvanese and G. De Giacomo, Reasoning on UML class diagrams, Artif. Intell. 168 (2005) 70–118. Crossref, Web of Science, Google Scholar
14. R. V. D. Straeten, T. Mens, J. Simmonds and V. Jonckers, Using Description Logic to Maintain Consistency between UML Models, The Unified Modeling Language, Modeling Languages and Applications (2003). Google Scholar
15. D. Jackson, Software Abstractions, Logic, Language, and Analysis (MIT Press, Cambridge, 2006). Google Scholar
16. K. Anastasakis, B. Bordbar, G. Georg and I. Ray, UML2Alloy: A Challenging Model Transformation, Int. Conf. on Model Driven Engineering Languages and Systems (2007). Google Scholar
17. E. Torlak and D. Jackson, Kodkod: A relational model finder, TACAS ser. Lecture Notes in Computer Science, eds. O. Grumberg and M. Huth (Springer, Heidelberg, 2007) 632–647. Google Scholar
18. M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla and R. Drechsler, Verifying UML/OCL models using Boolean satisfiability, Design, Automation and Test in Europe (2010). Google Scholar
19. N. Przigoda, R. Wille and R. Drechsler, Contradiction analysis for inconsistent UML/OCL models, IEEE Int. Symp. Des. Diagnostics Electron. Circuits & Syst. (DDECS) 2015 (2015) 171–176. Google Scholar
20. M. Gogolla and M. Richters, Expressing UML Class Diagrams Properties with OCL, Object Modeling with the OCL Ser. Lecture Notes in Computer Science eds., eds. T. Clark and J. Warmer (Springer, Germany, 2002), pp. 85–114. Crossref, Google Scholar
21. D. Steinberg, F. Budinsky, M. Paternostro and E. Merks, EMF: Eclipse Modeling Framework 2.0, 2nd edn. (Addison-Wesley Professional, 2009). Google Scholar
22. S. A. Cook, The complexity of theorem-proving procedures, in STOC71, Proc. Third Annual ACM Symp. on Theory comput. (1971). Google Scholar
23. R. Brummayer and A. Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, Tools and Algorithms for the Construction and Analysis of Systems Ser. Lecture Notes in Computer Science, eds. S. Kowalewski and A. Philippou (Springer, 2009) 174–177. Crossref, Google Scholar
24. Clark Barrett and Aaron Stump and Cesare Tinelli, The SMT-LIB Standard: Version 2.0, 2010, Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), A. Gupta and D. Kroening. Google Scholar
25. E. Torlak, F. S.-H. Chang and D. Jackson, Finding Minimal Unsatisfiable Cores of Declarative Specifications, Formal Methods 326–341. Google Scholar
26. R. Wille, M. Soeken and R. Drechsler, Debugging of inconsistent UML/OCL models, Design, Automation and Test in Europe, Dresden (2012). Google Scholar
27. J. Zhang, S. Shen, J. Zhang, W. Xu and S. Li, Extracting minimal unsatisfiable subformulas in satisfiability modulo theories, Comput. Sci. Inf. Syst. 8 (2011) 693–710. Crossref, Web of Science, Google Scholar
28. R. Gershman, M. Koifman and O. Strichman, An approach for extracting a small unsatisfiable core, Form. Methods Syst. Des. 33 (2008) 1–27. Crossref, Web of Science, Google Scholar
29. D. Große, R. Wille, R. Siegmund and R. Drechsler, Contradiction Analysis for Constraint-based Random Simulation, Forum on specification and Design Languages (2008) 130–135. Google Scholar