http://iet.metastore.ingenta.com
1887

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

  • HTML
    274.6689453125Kb
  • XML
    218.0888671875Kb
  • PDF
    707.37109375Kb
Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/1/1/IET-CPS.2016.0022.html;jsessionid=2gsmf3os1obnt.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2016.0022&mimeType=html&fmt=ahah

References

    1. 1)
      • 1. Rumbaugh, J., Jacobson, I., Booch, G.: ‘The unified modeling language reference manual’, 1999.
    2. 2)
      • 2. Object Management Group: ‘Object Constraint Language, 2014. Version 2.4’, February 2014.
    3. 3)
      • 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.
    4. 4)
    5. 5)
      • 5. Jackson, D.: ‘Software abstractions – logic, language, and analysis’ (MIT Press, 2006).
    6. 6)
      • 6. Soeken, M., Drechsler, R.: ‘Formal specification level – concepts, methods, and algorithms’ (Springer, 2015).
    7. 7)
      • 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.
    8. 8)
      • 8. Gogolla, M., Richters, M.: ‘Expressing UML class diagrams properties with OCL’. Object Modeling with the OCL, 2002, pp. 85114.
    9. 9)
      • 9. Steinberg, D., Budinsky, F., Paternostro, M., et al: ‘EMF: eclipse modeling framework 2.0’ (Addison-Wesley Professional, 2009, 2nd edn.).
    10. 10)
      • 10. Kosiuczenko, P.: ‘Specification of invariability in OCL’. Int. Conf. on Model Driven Engineering Languages and Systems, 2006, pp. 676691.
    11. 11)
    12. 12)
      • 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.
    13. 13)
      • 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.
    14. 14)
      • 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.
    15. 15)
      • 15. Cabot, J., Clarisó, R., Riera, D.: ‘Verification of UML/OCL class diagrams using constraint programming’. ICST Workshops, 2008, pp. 7380.
    16. 16)
    17. 17)
      • 17. Torlak, E., Jackson, D.: ‘Kodkod: a relational model finder’. Tools and Algorithms for Construction and Analysis of Systems, 2007, pp. 632647.
    18. 18)
      • 18. Gogolla, M., Kuhlmann, M., Hamann, L.: ‘Consistency, independence and consequences in UML and OCL models’. Tests and Proof, 2009, pp. 90104.
    19. 19)
      • 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.
    20. 20)
      • 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.
    21. 21)
      • 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.
    22. 22)
    23. 23)
      • 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.
    24. 24)
      • 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).
    25. 25)
      • 25. Malgouyres, H., Motet, G.: ‘A UML model consistency verification approach based on meta-modeling formalization’. ACM Symp. on Applied computing, 2006, pp. 18041809.
    26. 26)
      • 26. Mancini, T.: ‘Finite satisfiability of UML class diagrams by constraint programming’. Description Logics, 2004.
    27. 27)
    28. 28)
      • 28. Van Der Straeten, R., Mens, T., Simmonds, J., et al: ‘Using description logic to maintain consistency between UML models’. UML, 2003, pp. 326340.
    29. 29)
      • 29. Eén, N., Sörensson, N.: ‘An extensible SAT-solver’. SAT, 2003, pp. 502518.
    30. 30)
      • 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.
    31. 31)
      • 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.
    32. 32)
      • 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.
    33. 33)
      • 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.
    34. 34)
      • 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.
    35. 35)
      • 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.
    36. 36)
      • 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.
    37. 37)
      • 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.
    38. 38)
      • 38. Przigoda, N., Wille, R., Drechsler, R.: ‘Analyzing inconsistencies in UML/OCL models’, J. Circuits Syst. Comput., 2016.
    39. 39)
      • 39. Torlak, E., Chang, F.S.-H., Jackson, D.: ‘Finding minimal unsatisfiable cores of declarative specifications’. Formal Methods, 2008, pp. 326341.
    40. 40)
      • 40. Wille, R., Soeken, M., Drechsler, R.: ‘Debugging of inconsistent UML/OCL models’. Design, Automation and Test in Europe, 2012, pp. 10781083.
    41. 41)
      • 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.
    42. 42)
      • 42. Soeken, M., Wille, R., Drechsler, R.: ‘Verifying dynamic aspects of UML models’. Design, Automation and Test in Europe, 2011, pp. 10771082.
    43. 43)
      • 43. Delmas, R., Doose, D., Pires, A.F., et al: ‘Supporting model based design’. Int. Conf. on Model and Data Engineering, 2011, pp. 237248.
    44. 44)
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
This is a required field
Please enter a valid email address