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=1wt3c7leo6ou1.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2016.0022&mimeType=html&fmt=ahah

References

    1. 1)
      • J. Rumbaugh , I. Jacobson , G. Booch .
        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)
      • R.B. France , B. Rumpe .
        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.
        . Workshop on the Future of Software Engineering , 37 - 54
    4. 4)
    5. 5)
      • D. Jackson . (2006)
        5. Jackson, D.: ‘Software abstractions – logic, language, and analysis’ (MIT Press, 2006).
        .
    6. 6)
      • M. Soeken , R. Drechsler . (2015)
        6. Soeken, M., Drechsler, R.: ‘Formal specification level – concepts, methods, and algorithms’ (Springer, 2015).
        .
    7. 7)
      • M. Soeken , R. Wille , M. Kuhlmann .
        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.
        . Design, Automation and Test in Europe , 1341 - 1344
    8. 8)
      • M. Gogolla , M. Richters .
        8. Gogolla, M., Richters, M.: ‘Expressing UML class diagrams properties with OCL’. Object Modeling with the OCL, 2002, pp. 85114.
        . Object Modeling with the OCL , 85 - 114
    9. 9)
      • D. Steinberg , F. Budinsky , M. Paternostro . (2009)
        9. Steinberg, D., Budinsky, F., Paternostro, M., et al: ‘EMF: eclipse modeling framework 2.0’ (Addison-Wesley Professional, 2009, 2nd edn.).
        .
    10. 10)
      • P. Kosiuczenko .
        10. Kosiuczenko, P.: ‘Specification of invariability in OCL’. Int. Conf. on Model Driven Engineering Languages and Systems, 2006, pp. 676691.
        . Int. Conf. on Model Driven Engineering Languages and Systems , 676 - 691
    11. 11)
    12. 12)
      • P. Niemann , F. Hilken , M. Gogolla .
        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.
        . Design, Automation and Test in Europe , 309 - 312
    13. 13)
      • P. Niemann , F. Hilken , M. Gogolla .
        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.
        . Int. Conf. on Model Driven Engineering Languages and Systems , 266 - 275
    14. 14)
      • K. Anastasakis , B. Bordbar , G. Georg .
        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.
        . Int. Conf. on Model Driven Engineering Languages and Systems , 436 - 450
    15. 15)
      • J. Cabot , R. Clarisó , D. Riera .
        15. Cabot, J., Clarisó, R., Riera, D.: ‘Verification of UML/OCL class diagrams using constraint programming’. ICST Workshops, 2008, pp. 7380.
        . ICST Workshops , 73 - 80
    16. 16)
    17. 17)
      • E. Torlak , D. Jackson .
        17. Torlak, E., Jackson, D.: ‘Kodkod: a relational model finder’. Tools and Algorithms for Construction and Analysis of Systems, 2007, pp. 632647.
        . Tools and Algorithms for Construction and Analysis of Systems , 632 - 647
    18. 18)
      • M. Gogolla , M. Kuhlmann , L. Hamann .
        18. Gogolla, M., Kuhlmann, M., Hamann, L.: ‘Consistency, independence and consequences in UML and OCL models’. Tests and Proof, 2009, pp. 90104.
        . Tests and Proof , 90 - 104
    19. 19)
      • M. Gogolla , L. Hamann , F. Hilken .
        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.
        . Modellierung , 273 - 288
    20. 20)
      • F. Hilken , L. Hamann , M. Gogolla .
        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.
        . Int. Conf. on Theory and Practice of Model Transformations , 170 - 185
    21. 21)
      • F. Hilken , P. Niemann , M. Gogolla .
        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.
        . Tests and Proof , 99 - 116
    22. 22)
    23. 23)
      • A.D. Brucker , B. Wolff .
        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.
        . Theorem Proving in Higher Order Logics , 99 - 114
    24. 24)
      • B. Beckert , R. Hähnle , P.H. Schmitt . (2007)
        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)
      • H. Malgouyres , G. Motet .
        25. Malgouyres, H., Motet, G.: ‘A UML model consistency verification approach based on meta-modeling formalization’. ACM Symp. on Applied computing, 2006, pp. 18041809.
        . ACM Symp. on Applied computing , 1804 - 1809
    26. 26)
      • T. Mancini .
        26. Mancini, T.: ‘Finite satisfiability of UML class diagrams by constraint programming’. Description Logics, 2004.
        . Description Logics
    27. 27)
    28. 28)
      • R. Van Der Straeten , T. Mens , J. Simmonds .
        28. Van Der Straeten, R., Mens, T., Simmonds, J., et al: ‘Using description logic to maintain consistency between UML models’. UML, 2003, pp. 326340.
        . UML , 326 - 340
    29. 29)
      • N. Eén , N. Sörensson .
        29. Eén, N., Sörensson, N.: ‘An extensible SAT-solver’. SAT, 2003, pp. 502518.
        . SAT , 502 - 518
    30. 30)
      • R. Brummayer , A. Biere .
        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.
        . Tools and Algorithms for Construction and Analysis of Systems , 174 - 177
    31. 31)
      • R. Clarisó , C.A. González , J. Cabot .
        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.
        . Int. Conf. on Software Engineering and Formal Methods , 108 - 114
    32. 32)
      • M. Soeken , R. Wille , R. Drechsler .
        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.
        . Workshop on Model-Driven Engineering, Verification and Validation , 2:1 - 2:4
    33. 33)
      • M. Soeken , R. Wille , R. Drechsler .
        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.
        . Tests and Proof , 152 - 170
    34. 34)
      • N. Przigoda , R. Wille , R. Drechsler .
        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.
        . Int. Conf. on Model Driven Engineering Languages and Systems , 261 - 271
    35. 35)
      • N. Przigoda , J.G. Filho , P. Niemann .
        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.
        . Int. Conf. on Formal Methods and Models for System Design
    36. 36)
      • N. Przigoda , C. Hilken , R. Wille .
        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.
        . Int. Conf. on Model Driven Engineering Languages and Systems , 176 - 185
    37. 37)
      • N. Przigoda , R. Wille , R. Drechsler .
        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.
        . Int. Symp. on Design and Diagnostics of Electronic Circuits & Systems , 171 - 176
    38. 38)
      • N. Przigoda , R. Wille , R. Drechsler .
        38. Przigoda, N., Wille, R., Drechsler, R.: ‘Analyzing inconsistencies in UML/OCL models’, J. Circuits Syst. Comput., 2016.
        . J. Circuits Syst. Comput.
    39. 39)
      • E. Torlak , F.S.-H. Chang , D. Jackson .
        39. Torlak, E., Chang, F.S.-H., Jackson, D.: ‘Finding minimal unsatisfiable cores of declarative specifications’. Formal Methods, 2008, pp. 326341.
        . Formal Methods , 326 - 341
    40. 40)
      • R. Wille , M. Soeken , R. Drechsler .
        40. Wille, R., Soeken, M., Drechsler, R.: ‘Debugging of inconsistent UML/OCL models’. Design, Automation and Test in Europe, 2012, pp. 10781083.
        . Design, Automation and Test in Europe , 1078 - 1083
    41. 41)
      • L.M. de Moura , N. Bjørner .
        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.
        . Tools and Algorithms for Construction and Analysis of Systems , 337 - 340
    42. 42)
      • M. Soeken , R. Wille , R. Drechsler .
        42. Soeken, M., Wille, R., Drechsler, R.: ‘Verifying dynamic aspects of UML models’. Design, Automation and Test in Europe, 2011, pp. 10771082.
        . Design, Automation and Test in Europe , 1077 - 1082
    43. 43)
      • R. Delmas , D. Doose , A.F. Pires .
        43. Delmas, R., Doose, D., Pires, A.F., et al: ‘Supporting model based design’. Int. Conf. on Model and Data Engineering, 2011, pp. 237248.
        . Int. Conf. on Model and Data Engineering , 237 - 248
    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