access icon openaccess Verifying the structure and behavior in UML/OCL models using satisfiability solvers

Due to the ever increasing complexity of embedded and cyber-physical systems, corresponding design solutions relying on modelling languages such as Unified Modelling Language (UML)/Object Constraint Language (OCL) find increasing attention. Due to the recent success of formal verification techniques, UML/OCL models also allow to verify and/or check certain properties of a given model in early stages of the design phase. To this end, different approaches for verification and validation have been proposed. In this work, the authors motivate, define, and describe different verification tasks for structural, as well as behavioural UML/OCL models that can be solved using solvers for Boolean satisfiability. They describe how these verification tasks can be translated into a symbolic formulation which is passed to off-the-shelf solvers afterwards. The obtained results enable designers to draw conclusions about the correctness of the considered model.

Inspec keywords: Boolean functions; formal verification; computability; Unified Modeling Language

Other keywords: validation task; structural UML/OCL model; Unified Modelling Language/Object Constraint Language model; formal verification techniques; off-the-shelf solvers; behavioural UML/OCL model; symbolic formulation; Boolean satisfiability; satisfiability solvers

Subjects: Formal logic; Formal methods

References

    1. 1)
      • 6. Soeken, M., Drechsler, R.: ‘Formal specification level – concepts, methods, and algorithms’ (Springer, 2015).
    2. 2)
    3. 3)
      • 1. Rumbaugh, J., Jacobson, I., Booch, G.: ‘The unified modeling language reference manual’, 1999.
    4. 4)
      • 3. France, R.B., Rumpe, B.: ‘Model-driven development of complex software: a research roadmap’. Workshop on the Future of Software Engineering, 2007, pp. 3754.
    5. 5)
      • 33. Soeken, M., Wille, R., Drechsler, R.: ‘Encoding OCL data types for SAT-based verification of UML/OCL models’. Tests and Proof, 2011, pp. 152170.
    6. 6)
      • 23. Brucker, A.D., Wolff, B.: ‘A proposal for a formal OCL semantics in Isabelle/HOL’. Theorem Proving in Higher Order Logics, 2002, pp. 99114.
    7. 7)
      • 40. Wille, R., Soeken, M., Drechsler, R.: ‘Debugging of inconsistent UML/OCL models’. Design, Automation and Test in Europe, 2012, pp. 10781083.
    8. 8)
    9. 9)
      • 41. de Moura, L.M., Bjørner, N.: ‘Z3: an efficient SMT solver’. Tools and Algorithms for Construction and Analysis of Systems, 2008, pp. 337340.
    10. 10)
      • 14. Anastasakis, K., Bordbar, B., Georg, G., et al: ‘UML2Alloy: a challenging model transformation’. Int. Conf. on Model Driven Engineering Languages and Systems, 2007, pp. 436450.
    11. 11)
      • 9. Steinberg, D., Budinsky, F., Paternostro, M., et al: ‘EMF: eclipse modeling framework 2.0’ (Addison-Wesley Professional, 2009, 2nd edn.).
    12. 12)
      • 19. Gogolla, M., Hamann, L., Hilken, F., et al: ‘From application models to filmstrip models: an approach to automatic validation of model dynamics’. Modellierung, 2014, pp. 273288.
    13. 13)
      • 17. Torlak, E., Jackson, D.: ‘Kodkod: a relational model finder’. Tools and Algorithms for Construction and Analysis of Systems, 2007, pp. 632647.
    14. 14)
      • 29. Eén, N., Sörensson, N.: ‘An extensible SAT-solver’. SAT, 2003, pp. 502518.
    15. 15)
      • 43. Delmas, R., Doose, D., Pires, A.F., et al: ‘Supporting model based design’. Int. Conf. on Model and Data Engineering, 2011, pp. 237248.
    16. 16)
    17. 17)
      • 24. Beckert, B., Hähnle, R., Schmitt, P.H.: ‘Verification of object-oriented software: The KeY approach’ (Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2007).
    18. 18)
    19. 19)
      • 25. Malgouyres, H., Motet, G.: ‘A UML model consistency verification approach based on meta-modeling formalization’. ACM Symp. on Applied computing, 2006, pp. 18041809.
    20. 20)
      • 13. Niemann, P., Hilken, F., Gogolla, M., et al: ‘Extracting frame conditions from operation contracts’. Int. Conf. on Model Driven Engineering Languages and Systems, 2015, pp. 266275.
    21. 21)
      • 28. Van Der Straeten, R., Mens, T., Simmonds, J., et al: ‘Using description logic to maintain consistency between UML models’. UML, 2003, pp. 326340.
    22. 22)
      • 36. Przigoda, N., Hilken, C., Wille, R., et al: ‘Checking concurrent behavior in UML/OCL models’. Int. Conf. on Model Driven Engineering Languages and Systems, 2015, pp. 176185.
    23. 23)
      • 21. Hilken, F., Niemann, P., Gogolla, M., et al: ‘Filmstripping and unrolling: a comparison of verification approaches for UML and OCL behavioral models’. Tests and Proof, 2014, pp. 99116.
    24. 24)
      • 8. Gogolla, M., Richters, M.: ‘Expressing UML class diagrams properties with OCL’. Object Modeling with the OCL, 2002, pp. 85114.
    25. 25)
      • 34. Przigoda, N., Wille, R., Drechsler, R.: ‘Ground setting properties for an efficient translation of OCL in SMT-based model finding’. Int. Conf. on Model Driven Engineering Languages and Systems, 2016, pp. 261271.
    26. 26)
      • 18. Gogolla, M., Kuhlmann, M., Hamann, L.: ‘Consistency, independence and consequences in UML and OCL models’. Tests and Proof, 2009, pp. 90104.
    27. 27)
      • 20. Hilken, F., Hamann, L., Gogolla, M.: ‘Transformation of UML and OCL models into filmstrip models’. Int. Conf. on Theory and Practice of Model Transformations, 2014, pp. 170185.
    28. 28)
      • 31. Clarisó, R., González, C.A., Cabot, J.: ‘Towards domain refinement for UML/OCL bounded verification’. Int. Conf. on Software Engineering and Formal Methods, 2015, pp. 108114.
    29. 29)
    30. 30)
      • 35. Przigoda, N., Filho, J.G., Niemann, P., et al: ‘Frame conditions in symbolic representations of UML/OCL models’. Int. Conf. on Formal Methods and Models for System Design, 2016.
    31. 31)
      • 5. Jackson, D.: ‘Software abstractions – logic, language, and analysis’ (MIT Press, 2006).
    32. 32)
      • 30. Brummayer, R., Biere, A.: ‘Boolector: an efficient SMT solver for bit-vectors and arrays’. Tools and Algorithms for Construction and Analysis of Systems, 2009, pp. 174177.
    33. 33)
      • 7. Soeken, M., Wille, R., Kuhlmann, M., et al: ‘Verifying UML/OCL models using Boolean satisfiability’. Design, Automation and Test in Europe, 2010, pp. 13411344.
    34. 34)
      • 32. Soeken, M., Wille, R., Drechsler, R.: ‘Towards automatic determination of problem bounds for object instantiation in static model verification’. Workshop on Model-Driven Engineering, Verification and Validation, 2011, pp. 2:12:4.
    35. 35)
    36. 36)
      • 26. Mancini, T.: ‘Finite satisfiability of UML class diagrams by constraint programming’. Description Logics, 2004.
    37. 37)
      • 10. Kosiuczenko, P.: ‘Specification of invariability in OCL’. Int. Conf. on Model Driven Engineering Languages and Systems, 2006, pp. 676691.
    38. 38)
      • 39. Torlak, E., Chang, F.S.-H., Jackson, D.: ‘Finding minimal unsatisfiable cores of declarative specifications’. Formal Methods, 2008, pp. 326341.
    39. 39)
      • 42. Soeken, M., Wille, R., Drechsler, R.: ‘Verifying dynamic aspects of UML models’. Design, Automation and Test in Europe, 2011, pp. 10771082.
    40. 40)
      • 38. Przigoda, N., Wille, R., Drechsler, R.: ‘Analyzing inconsistencies in UML/OCL models’, J. Circuits Syst. Comput., 2016.
    41. 41)
      • 15. Cabot, J., Clarisó, R., Riera, D.: ‘Verification of UML/OCL class diagrams using constraint programming’. ICST Workshops, 2008, pp. 7380.
    42. 42)
      • 37. Przigoda, N., Wille, R., Drechsler, R.: ‘Contradiction analysis for inconsistent formal models’. Int. Symp. on Design and Diagnostics of Electronic Circuits & Systems, 2015, pp. 171176.
    43. 43)
      • 2. Object Management Group: ‘Object Constraint Language, 2014. Version 2.4’, February 2014.
    44. 44)
      • 12. Niemann, P., Hilken, F., Gogolla, M., et al: ‘Assisted generation of frame conditions for formal models’. Design, Automation and Test in Europe, 2015, pp. 309312.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2016.0022
Loading

Related content

content/journals/10.1049/iet-cps.2016.0022
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading