A Symbolic Formulation for Models

In this chapter, we present a symbolic formulation representing all system states of a given UML/OCL model. We thereby do not only consider the usually assumed 2-valued logic, but also a 4-valued logic which additionally can handle null and invalid. To set the context, first the overall flow for validation and verification of UML/OCL models is reviewed. Afterwards, the detailed transformation of an arbitrarily given UML/OCL model to a symbolic representation is provided. This is then used, to employ the respective verification tasks which is briefly sketched but outlined in more detail in the following chapters. The end of this chapter provides a brief summary of other and similar approaches for UML/OCL validation and verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic €32.70 /Month

Buy Now

Price includes VAT (France)

eBook EUR 117.69 Price includes VAT (France)

Softcover Book EUR 158.24 Price includes VAT (France)

Hardcover Book EUR 158.24 Price includes VAT (France)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Notes

The term model finding comes from the fact that models as introduced in Chap. 2 are also called meta-models and the instances of those meta-models are consequently also called models.

More details will be discussed later in Sect. 3.4.

The problem bounds will be extended later, e.g., for providing an interval instead of only a fixed number for the object instances or the number of system states, when a sequence of system states is considered.

The restriction of the position index (cf. Lines 36–39 in the following listing) is not necessary, since the sum of all other constraints already implies it. However, the position index restricting constraints are added to provide more information to the used SMT solver.

Without loss of generality, it is assumed that the first k sub bits of \(\beta _>\) are belonging to the objects in \(\varUpsilon _>\) .

For Boolean attributes the 0 in the conclusion has to be replaced by false and for class attributes the changed type from Transformation Rule 7 is used again, i.e., \(\alpha _^<\upsilon >: \varUpsilon _\mapsto \mathbb\) . In the latter case, α a υ = 0 means that the function always evaluates to false .

The differentiation for the upper bounds ≤ 1 and > 1 is caused by a technical detail in the UML and OCL standards.

The details have been omitted in Fig. 3.6 to keep it clearer, however, interested readers are referred to [Obj14, Fig. 8.4 and 13.5 on pp. 50 and 201].

Note that the textual definition is equivalent to the respective truth tables—provided the “either …or” is meant as a logical or—, but it is not equivalent to the definition via postcondition, see also Appendix C.

Quote from the OCL spec: “A PropertyCallExpression is a reference to an Attribute of a Classifier defined in a UML model. It evaluates to the value of the attribute.”

This can be easily done using extract and maybe concat afterwards.

If a sOrderedSet or a sSequence is called on an un-ordered collection type like set of bag, the resulting collection type can have any order unless all elements are contained.

In the following, the terms lower and upper bound are frequently used for both, the fixed number of objects and the interval. For a fixed number of objects, the number itself can be seen as the lower and the upper bound simultaneously.

Note that the cited works are using the terms weak and strong satisfiability of a model instead of consistency. However, in order to avoid confusion with the satisfiability of SAT or SMT instances this book uses weak and strong consistency.

For the sake of convenience, only regular values are considered for the attributes.

With \(\boldsymbol<\omega >_\) the precise operation call of the transition from σ i to σ i+1 is meant, while the set of all operation calls is \(\varOmega _ =\<\omega _<0>,\omega _,\ldots,\omega _<\vert \varOmega _\vert -1>\>\) .

If the system states are numbered, instead of \(\boldsymbol<\omega >_\) also \(\boldsymbol<\omega >_\) is used for the transition between σ i and σ i+1.

Please note that the following descriptions of tools are partially taken from the corresponding websites.

Available at http://www.mpkrieger.net/oclsolve/. Available at http://www.sat4j.org/. Available at http://minisat.se. Available at http://www.cs.bham.ac.uk/~bxb/UML2Alloy. Available at http://alloy.mit.edu/alloy/. Available at http://alloy.mit.edu/kodkod. Available at https://github.com/SOM-Research/EMFtoCSP. Available at http://gres.uoc.edu/UMLtoCSP/. Available at http://eclipseclp.org. Available at http://software.imdea.org/~dania/tools/ocl2msfol.html. Available at http://www.actiongui.org/index.php/new-ocl2fol-menu. Available at http://www.actiongui.org/index.php/ocl2fol-project. Available at https://www.brucker.ch/projects/hol-ocl/. Available at http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html. Available at http://pvs.csl.sri.com.

References

  1. J.-R. Abrial, System Study: Method and Example, 1999. URL:http://atelierb.eu/ressources/PORTES/Texte/porte.anglais.ps.gz
  2. P.G. de Aledo, P. Sánchez Espeso, FramewORk for embedded system - verification (competition contribution), in Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015, Proceedings, vol. 9035. Lecture Notes in Computer Science, 2015, pp. 429–431. doi:10.1007/978-3-662-46681-0_36 Google Scholar
  3. P.G. de Aledo, P. Sánchez Espeso, R. Huuck, An approach to static-dynamic software analysis, in Formal Techniques for Safety-Critical Systems - Fourth International Workshop, FTSCS 2015, Paris, France, November 6–7, 2015. Revised Selected Papers, vol. 596. Communications in Computer and Information Science, 2015, pp. 225–240 Google Scholar
  4. W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, P.H. Schmitt, The KeY tool. Softw. Syst. Model. 4(1), 32–54 (2005). doi:10.1007/s10270-004-0058-x ArticleGoogle Scholar
  5. P.G. de Aledo, N. Przigoda, R. Wille, R. Drechsler, P. Sánchez Espeso, Towards a verification flow across abstraction levels verifying implementations against their formal specification. IEEE Trans. CAD Integr. Circuits Syst. 36(3), 475–488 (2017). doi:10.1109/TCAD.2016.2611494 Google Scholar
  6. C. André, F. Mallet, Clock Constraints in UML/MARTE CCSL. Tech. rep. RR-6540, 2008. URL:https://hal.inria.fr/inria-00280941/file/rr-6540.pdf
  7. C. André, F. Mallet, J. DeAntoni, VHDL observers for clock constraint checking, in IEEE Fifth International Symposium on Industrial Embedded Systems, SIES 2010, University of Trento, Italy, July 7–9, 2010, pp. 98–107. doi:10.1109/SIES.2010.5551372 Google Scholar
  8. K. Anastasakis, B. Bordbar, G. Georg, I. Ray, UML2Alloy: A challenging model transformation, in Model Driven Engineering Languages and Systems, 10th International Conference, MoDELS 2007, Nashville, USA, September 30–October 5, 2007, Proceedings, vol. 4735. Lecture Notes in Computer Science, 2007, pp. 436–450. doi:10.1007/978-3-540-75209-7_30 Google Scholar
  9. C. Barrett, C.L. Conway Morgan Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, C. Tinelli, CVC4, in Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011, Proceedings, vol. 6806. Lecture Notes in Computer Science, 2011, pp. 171–177. doi:10.1007/978-3-642-22110-1_14 Google Scholar
  10. R. Brummayer, A. Biere, Boolector: An efficient SMT solver for bit-vectors and arrays, in Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22–29, 2009, Proceedings, vol. 5505. Lecture Notes in Computer Science, 2009, pp. 174–177. doi:10.1007/978-3-642-00768-2_16 Google Scholar
  11. D. Berardi, D. Calvanese, G. De Giacomo, Reasoning on UML class diagrams. Artif. Intell. 168(1–2), 70–118 (2005). doi:10.1016/j.artint.2005.05.003 ArticleMathSciNetMATHGoogle Scholar
  12. C. Barrett, P. Fontaine, C. Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB), 2016. URL:http://www.SMT-LIB.org
  13. B. Beckert, R. Hähnle, P.H. Schmitt, Verification of Object-Oriented Software: The KeY Approach, 2007. doi:10 1007/978-3-540-69061-0 Google Scholar
  14. A. Biere, M. Heule, H. van Maaren, T. Walsh, Handbook of Satisfiability, Amsterdam, The Netherlands, 2009. ISBN: 9781586039295 MATHGoogle Scholar
  15. A. Borgida, J. Mylopoulos, R. Reiter, On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785–798 (1995). doi:10.1109/32.469460 ArticleGoogle Scholar
  16. R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani, The MathSAT 4SMT Solver, in Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7–14, 2008, Proceedings, vol. 5123. Lecture Notes in Computer Science, 2008, pp. 299–303. doi:10.1007/978-3-540-70545-1_28 Google Scholar
  17. B. Beckert, P.H. Schmitt, Program verification using change information, in 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 22–27 September 2003, Brisbane Australia, 2003, p. 91. doi:10.1109/SEFM.2003.1236211 Google Scholar
  18. A.D. Brucker, F. Tuong, B. Wolff, Feather-weight OCL: A proposal for a machine-checked formal semantics for OCL 2.5, in Archive of Formal Proofs 2014, 2014. URL:https://www.isa-afp.org/entries/Featherweight_OCL.shtml
  19. S. Bucur, V. Ureche, C. Zamfir, G. Candea, Parallel symbolic execution for automated real-world software testing, in European Conference on Computer Systems, Proceedings of the Sixth European conference on Computer systems, EuroSys 2011, Salzburg, Austria, April 10–13, 2011, 2011, pp. 183–198. doi:10.1145/1966445.1966463 Google Scholar
  20. A.D. Brucker, B. Wolff, Semantics, calculi, and analysis for object-oriented specifications. Acta Inf. 46(4), 255–284 (2009). doi:10.1007/s00236-009-0093-8 ArticleMathSciNetMATHGoogle Scholar
  21. J. Cabot, Ambiguity issues in OCL postconditions, in OCL Workshop, 2006, pp. 194–204 Google Scholar
  22. J. Cabot, From declarative to imperative UML/OCL operation specifications, in Conceptual Modeling ER - 2007, 26th International Conference on Conceptual Modeling, Auckland, New Zealand, November 5–9, 2007, Proceedings, vol. 4801. Lecture Notes in Computer Science, 2007, pp. 198–213. doi:10.1007/978-3-540-75563-0_15 Google Scholar
  23. J. Cabot, R. Clarisó, D. Riera, UMLtoCSP: a tool for the formal verification of UML/OCL models using constraint programming, in 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), November 5–9, 2007, Atlanta, Georgia, USA, 2007, pp. 547–548 Google Scholar
  24. J. Cabot, R. Clarisó, D. Riera, Verification of UML/OCL class diagrams using constraint programming, in First International Conference on Software Testing Verification and Validation, ICST 2008, Lillehammer Norway, April 9–11, 2008, Workshops, Proceedings, 2008, pp. 73–80 Google Scholar
  25. J. Cabot, R. Clarisó, D. Riera, Verifying UML/OCL operation contracts, in Integrated Formal Methods, 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16–19, 2009, Proceedings, vol. 5423. Lecture Notes in Computer Science, 2009, pp. 40–55. doi:10.1007/978-3-642-00255-7_4 Google Scholar
  26. J. Cabot, R. Clarisó, D. Riera, On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014). doi:10.1016/j.jss.2014.03.023 ArticleGoogle Scholar
  27. C. Cadar, D. Dunbar, D.R. Engler, KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, in 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8–10, 2008, San Diego, California, USA, Proceedings, 2008, pp. 209–224. URL:http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf
  28. M. Clavel, M. Egea, M. Angel García de Dios, Checking unsatisfiability for OCL constraints. ECEASST 24 (2009). URL:http://journal.ub.tuberlin.de/index.php/eceasst/article/view/334
  29. R. Clarisó, C.A. González, J. Cabot, Towards domain refinement for UML/OCL bounded verification, in Software Engineering and Formal Methods - 13th International Conference SEFM 2015, York, UK, September 7–11, 2015, Proceedings, vol. 9276. Lecture Notes in Computer Science, 2015, pp. 108–114. doi:10.1007/978-3-319-22969-0_8 Google Scholar
  30. A. Cimatti, A. Griggio, B. Schaafsma, R. Sebastiani, The MathSAT5 SMT solver, in Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16–24, 2013, Proceedings, vol. 7795. Lecture Notes in Computer Science, 2013, pp. 93–107. doi:10.1007/978-3-642-36742-7_7 Google Scholar
  31. E.M. Clarke, D. Kroening, F. Lerda, A tool for checking ANSI-C programs, in Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS, 2004, Barcelona, Spain, March 29–April 2, 2004, Proceedings, vol. 2988. Lecture Notes in Computer Science, 2004, pp. 168–176. doi:10.1007/978-3-540-24730-2_15 Google Scholar
  32. S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of the Symposium on Theory of Computing, 1971, pp. 151–158. doi:10.1145/800157.805047 Google Scholar
  33. C. Dania, M. Clavel, OCL2FOL+: coping with undefinedness, in Proceedings of the MODELS 2013 OCL Workshop colocated with the 16th International ACM/IEEE Conference on Model Driven Engineering Languages and Systems (MODELS 2013), Miami, USA, September 30, 2013, vol. 1092. CEUR Workshop Proceedings, 2013, pp. 53–62. URL:http://ceur-ws.org/Vol-1092/dania.pdf
  34. C. Dania, M. Clavel, OCL2MSFOL: A mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints, in 19th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MoDELS 2015, Saint-Malo, Brittany France, October 2–7, 2016, 2016, pp. 65–75 Google Scholar
  35. M.A.G. de Dios, C. Dania, D.A. Basin, M. Clavel, Model-driven development of a secure eHealth application, in Engineering Secure Future Internet Services and Systems - Current Research, vol. 8431. Lecture Notes in Computer Science, 2014, pp. 97–118. doi:10.1007/978-3-319-07452-8_4 Google Scholar
  36. S. Disch, C. Scholl, Combinational equivalence checking using incremental SAT solving, output ordering, and resets, in Proceedings of the 12th Conference on Asia South Pacific Design Automation, ASP-DAC 2007, Yokohama, Japan, January 23–26, 2007, 2007, pp. 938–943. doi:10.1109/ASPDAC2007.358110 Google Scholar
  37. R. Drechsler, M. Soeken, R. Wille, Formal specification level: towards verification-driven design based on natural language processing, in Proceeding of the 2012 Forum on Specification and Design Languages, Vienna, Austria, September 18–20, 2012, 2012, pp. 53–58. URL:http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=6336984
  38. B. Demuth, C. Wilke, Model and object verification by using Dresden OCL, in Proceedings of the Russian-German Work-shop Innovation Information Technologies: Theory and Practice Ufa, Russia, 2009, pp. 687–690 Google Scholar
  39. E.S.M. Ebeid, D. Quaglia, F. Fummi, Generation of systemC/TLM code from UML/MARTE sequence diagrams for verification, in IEEE 15th International Symposium on Design and Diagnostics of Electronic Circuits & Systems, DDECS 2012, Tallinn, Estonia, April 18–20, 2012, 2012, pp. 187–190. doi:10.1109/DDECS.2012.6219051 Google Scholar
  40. G. Engels, C. Soltenborn, H. Wehrheim, Analysis of UML activities using dynamic meta modeling, in Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference FMOODS 2007, Paphos, Cyprus, June 6–8, 2007, Proceedings, vol. 4468. Lecture Notes in Computer Science, 2007, pp. 76–90. doi:10.1007/978-3-540-72952-5_5 Google Scholar
  41. S. Eggersglüß, R. Wille, R. Drechsler, Improved SAT-based ATPG: more constraints, better compaction, in The IEEE/ACM International Conference on Computer-Aided Design, IC-CAD’13, San Jose, CA, USA, November 18–21, 2013, 2013, pp. 85–90. doi:10.1109/ICCAD.2013.6691102 Google Scholar
  42. B. Finkbeiner, S. Schewe, SMT-Based Synthesis of Distributed Systems, in Second Workshop on Automated Formal Methods (AFM), November 6, 2007, Atlanta, Georgia, 2007, pp. 69–76 Google Scholar
  43. M. Gogolla, J. Bohling, M. Richters, Validation of UML and OCL models by automatic snapshot generation, in “UML” 2003 - The Unified Modeling Language, Modeling Languages and Applications, 6th International Conference, San Francisco, CA, USA, October 20–24, 2003, Proceedings, vol. 2863. Lecture Notes in Computer Science, 2003, pp. 265–279. doi:10.1007/978-3-540-45221-8_23 Google Scholar
  44. M. Gogolla, J. Bohling, M. Richters, Validating UML and OCL models in USE by automatic snapshot generation. Softw. Syst. Model. 4(4), 386–398 (2005). doi:10.1007/s10270-005-0089-y ArticleGoogle Scholar
  45. M. Gogolla, F. Büttner, M. Richters, USE: A UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007). doi:10.1016/j.scico.2007.01.013 ArticleMathSciNetMATHGoogle Scholar
  46. C.A. González, J. Cabot, Formal verification of static software models in MDE: A systematic review. Inf. Softw. Technol. 56(8), 821–838 (2014). doi:10.1016/j.infsof.2014.03.003 ArticleGoogle Scholar
  47. M. Gogolla, L. Hamann, M. Kuhlmann, Proving and visualizing OCL invariant independence by automatically generated test cases, in Tests and Proofs, 4th International Conference TAP 2010, Málaga, Spain, July 1–2, 2010, Proceedings, vol. 6143. Lecture Notes in Computer Science, 2010, pp. 38–54. doi:10.1007/978-3-642-13977-2_5 Google Scholar
  48. M. Gogolla, M. Kuhlmann, L. Hamann, Consistency independence and consequences in UML and OCL models, in Tests and Proofs, Third International Conference, TAP 2009, Zurich, Switzerland, July 2–3, 2009, Proceedings, vol. 5668. Lecture Notes in Computer Science, 2009, pp. 90–104. doi:10.1007/978-3-642-02949-3_8 Google Scholar
  49. P. Godefroid, N. Klarlund, K. Sen, DART: directed automated random testing, in Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12–15, 2005, 2005, pp. 213–223. doi:10.1145/1065010.1065036 Google Scholar
  50. R. Gershman, M. Koifman, O. Strichman, An approach for extracting a small unsatisfiable core. Formal Methods Syst. Des. 33(1–3), 1–27 (2008). doi:10.1007/s10703-008-0051-z ArticleMATHGoogle Scholar
  51. D. Große, H. Minh Le, R. Drechsler, Proving transaction and system-level properties of untimed SystemC TLM designs, in 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), Grenoble France 26–28 July 201, 2010, pp. 113–122. doi:10.1109/MEMCOD2010.5558643 Google Scholar
  52. J.F. Groote, M. Reza Mousavi, Modeling and Analysis of Communicating Systems, 2014. ISBN:9780262027717. URL:https://mitpress.mit.edu/books/modeling-and-analysis-communicating-systems
  53. M. Gogolla, L. Hamann, F. Hilken, M. Kuhlmann, R.B. France, From application models to filmstrip models: An approach to automatic validation of model dynamics, in Modellierung 2014, 19.–21. März 2014, Wien, Österreich, vol. 225. LNI. 2014, pp. 273–288 Google Scholar
  54. M. Gogolla, A. Vallecillo, L. Burgueño, F. Hilken, Employing classifying terms for testing model transformations, in 18th ACM/IEEE International Conference on Model Driven Engineer ing Languages and Systems, MoDELS 2015, Ottawa, ON, Canada, September–30 October 2, 2015, 2015, pp. 312–321. doi:10 1109/MODELS.2015.7338262 Google Scholar
  55. E.I. Goldberg, M.R. Prasad, R.K. Brayton, Using SAT for combinational equivalence checking, in Proceedings of the Conference on Design, Automation and Test in Europe, DATE 2001, Munich, Germany March 12–16, 2001, 2001, pp. 114–121. doi:10.1109/DATE.2001.915010 Google Scholar
  56. M. Gogolla, M. Richters, Expressing UML class diagrams properties with OCL, in Object Modeling with the OCL, The Rationale behind the Object Constraint Language, vol. 2263. Lecture Notes in Computer Science, 2002, pp. 85–114 Google Scholar
  57. M. Gogolla, M. Richters, Expressing UML class diagrams properties with OCL, in Object Modeling with the OCL, The Rationale behind the Object Constraint Language, vol. 2263. Lecture Notes in Computer Science, 2002, pp. 85–114. doi:10.1007/3540-45669-4_6 Google Scholar
  58. D. Große, R. Wille, R. Siegmund, R. Drechsler, Contradiction analysis for constraint-based random simulation, in Forum on Specification and Design Languages, FDL 2008, September 23–25, 2008, Stuttgart, Germany, Proceedings, 2008, pp. 130–135. doi:10.1109/FDL.2008.4641434 Google Scholar
  59. D. Harel, Statecharts: A visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987). doi:10.1016/0167-6423(87)90035-9 ArticleMathSciNetMATHGoogle Scholar
  60. F. Hilken, L. Hamann, M. Gogolla, Transformation of UML and OCL models into filmstrip models, in Theory and Practice of Model Transformations - 7th International Conference, ICMT 2014, Held as Part of STAF 2014, York, UK, July 21–22, 2014, Proceedings, vol. 8568. Lecture Notes in Computer Science, 2014, pp. 170–185. doi:10.1007/978-3-319-08789-4_13 Google Scholar
  61. C. Hilken, J. Seiter, R. Wille, U. Kühne, R. Drechsler, Verifying consistency between activity diagrams and their corresponding OCL contracts, in Proceedings of the 2014 Forum on Specification and Design Languages, FDL 2014, Munich, Germany, October 14–16, 2014, 2014, pp. 1–7. doi:10.1109/FDL2014.7119340 Google Scholar
  62. F. Hilken, P. Niemann, M. Gogolla, R. Wille, Filmstripping and unrolling: A comparison of verification approaches for UML and OCL behavioral models, in Tests and Proofs - 8th International Conference TAP 2014, Held as Part of STAF 2014, York, UK, July 24–25, 2014, Proceedings, vol. 8570. Lecture Notes in Computer Science, 2014, pp. 99–116. doi:10.1007/978-3-642-21768-5_12 Google Scholar
  63. D. Harel, A. Naamad, The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 293–333 (1996). doi:10.1145/235321.235322 ArticleGoogle Scholar
  64. W.-l. Huang, J. Peleska, U. Schulze, Test Automation Support. Tech. rep. D34.1. COMPASS comprehensive modelling for advanced systems of systems, 2013. URL:http://www.compass-research.eu/deliverables.html
  65. C. Hilken, J. Peleska, R. Wille, A unified formulation of behavioral semantics for SysML models, in MODELSWARD 2015 - Proceedings of the 3rd International Conference on Model-Driven Engineering and Software Development, ESEO, Angers, Loire Valley, France, 9–11 February, 2015, 2015, pp. 263–271. doi:10.5220/0005241602630271 Google Scholar
  66. A. Ignatiev, A. Previti, M.H. Liffiton, J. Marques-Silva, Smallest MUS extraction with minimal hitting set dualization, in Principles and Practice of Constraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August–31 September 4, 2015, Proceedings, vol. 9255. Lecture Notes in Computer Science, 2015, pp. 173–182. doi:10.1007/978-3-319-23219-5_13 Google Scholar
  67. D. Jackson, Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256–290 (2002). doi:10.1145/505145.505149 ArticleGoogle Scholar
  68. D. Jackson, Alloy: A new technology for software modelling, in Tools and Algorithms for the Construction and Analysis of Systems, 8th International Conference, TACAS 2002, Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8–12, 2002, Proceedings, vol. 2280. Lecture Notes in Computer Science, 2002, p. 20. doi:10.1007/3-540-46002-0_2 Google Scholar
  69. D. Jackson, Software Abstractions - Logic, Language, and Analysis, 2012, pp. I–XVI, 1–350. ISBN: 978-0-262-10114-1 Google Scholar
  70. R.M. Karp, Reducibility among combinatorial problems, in Proceedings of a Symposium on the Complexity of Computer Computations, held March 20–22, 1972, at the IBM Thomas J Watson Research Center Yorktown Heights, New York. The IBM Research Symposia Series, 1972, pp. 85–103. URL:http://www.cs.berkeley.edu/~luca/cs172/karp.pdf
  71. M. Kuhlmann, M. Gogolla, From UML and OCL to relational logic and back, in Model Driven Engineering Languages and Systems - 15th International Conference, MODELS 2012, Innsbruck, Austria, September 30–October 5, 2012, Proceedings, vol. 7590. Lecture Notes in Computer Science, 2012, pp. 415–431. doi:10.1007/978-3-642-33666-9_27 Google Scholar
  72. A. Knapp, S. Merz, Model checking and code generation for UML state machines and collaborations, in 2002, pp. 59–64 Google Scholar
  73. P. Kosiuczenko, Specification of invariability in OCL, in Model Driven Engineering Languages and Systems, 9th International Conference, MoDELS 2006, Genova, Italy, October 1–6, 2006, Proceedings, vol. 4199. Lecture Notes in Computer Science, 2006, pp. 676–691. doi:10.1007/11880240_47 Google Scholar
  74. P. Kosiuczenko, Specification of invariability in OCL – specifying invariable system parts and views. Softw. Syst. Model. 12(2), 415–434 (2013). doi:10.1007/s10270-011-0215-y ArticleMathSciNetGoogle Scholar
  75. D. Kroening, M. Tautschnig, CBMC - C bounded model checker - (competition contribution), in Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference. TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014, Proceedings, vol. 8413. Lecture Notes in Computer Science, 2014, pp. 389–391. doi:10.1007/9783-642-54862-8_26 Google Scholar
  76. M. Kyas, H. Fecher, F.S. de Boer, J. Jacob, J. Hooman, M. van der Zwaag, T. Arons, H. Kugler, Formalizing UML models and OCL constraints in PVS. Electr. Notes Theor. Comput. Sci. 115, 39–47 (2005). doi:10.1016/j.entcs.2004.09.027 ArticleGoogle Scholar
  77. C. Lattner, V.S. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, in 2nd IEEE/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20–24 March 2004, San Jose CA, USA, 2004, pp. 75–88. doi:10.1109/CGO.2004.1281665 Google Scholar
  78. H.M. Le, D. Große, V. Herdt, R. Drechsler, Verifying SystemC using an intermediate verification language and symbolic simulation, in The 50th Annual Design Automation Conference 2013, DAC ‘13, Austin, TX, USA, May 29–June 07, 2013, 2013, pp. 116:1–116:6. doi:10.1145/2463209.2488877 Google Scholar
  79. K.R.M. Leino, This Is Boogie 2. Tech. rep. 2008. URL:http://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf
  80. M.H. Liffiton, A. Previti, A. Malik, J. Marques-Silva, Fast, flexible MUS enumeration. Constraints 21(2), 223–250 (2016). doi:10.1007/s10601-015-9183-0 ArticleMathSciNetMATHGoogle Scholar
  81. X. Li, Z. Liu, J. He, Consistency checking of UML tequirements, in 10th International Conference on Engineering of Complex Computer Systems (ICECCS 2005), 16–20 June 2005, Shanghai, China, 2005, pp. 411–420. doi:10.1109/ICECCS.2005.28 Google Scholar
  82. D. Latella, I. Majzik, M. Massink, Towards a formal operational semantics of UML statechart diagrams, in Formal Methods for Open Object-Based Distributed Systems, IFIF TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), February 15–18, 1999, Florence Italy, vol. 139. IFIP Conference Proceedings, 1999 Google Scholar
  83. J. Lilius, I. Paltor, vUML: A tool for verifying UML models, in The 14th IEEE International Conference on Automated Software Engineering ASE 1999, Cocoa Beach, Florida, USA, 12–15 October 1999, 1999, pp. 255–258. doi:10.1109/ASE1999.802301 Google Scholar
  84. L.M. de Moura, N. Bjørner, Z3: An efficient SMT solver, in Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary March 29–April 6, 2008, Proceedings, vol. 4963. Lecture Notes in Computer Science, 2008, pp. 337–340. doi:10.1007/978-3-540-78800-3_24 Google Scholar
  85. R. Moiseev Shinpei Hayashi, M. Saeki, Generating assertion code from OCL: A transformational approach based on similarities of implementation languages, in Model Driven Engineering Languages and Systems, 12th International Conference MODELS 2009, Denver, CO, USA, October 4–9, 2009, Proceedings, vol. 5795. Lecture Notes in Computer Science, 2009, pp. 650–664. doi:10.1007/978-3-642-04425-0_52 Google Scholar
  86. J. Marques-Silva, M. Janota, A. Belov, Minimal sets over monotone predicates in boolean formulae, in Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13–19, 2013, Proceedings, vol. 8044. Lecture Notes in Computer Science, 2013, pp. 592–607. doi:10.1007/9783-642-39799-8_39 Google Scholar
  87. B. Meyer, J.-M. Nerson, M. Matsuo, EIFFEL: object-oriented design for software engineering, in ESEC ‘87, 1st European Software Engineering Conference, Strasbourg, France, September, 9–11, 1987, Proceedings, vol. 289. Lecture Notes in Computer Science, 1987, pp. 221–229. doi:10.1007/BFb0022115 Google Scholar
  88. F. Mallet, L. Yin, Correct Transformation from CCSL to Promela for Verification. Tech. rep. RR-7491, 2012, p. 33. URL:https://hal.inria.fr/hal-00667849/file/RR-7491.pdf
  89. A. Nöhrer, A. Biere, A. Egyed, Managing SAT inconsistencies with HUMUS, in Sixth International Workshop on Variability Modelling of Software-Intensive Systems, Leipzig, Germany, January 25–27, 2012, Proceedings, 2012, pp. 83–91 Google Scholar
  90. P. Niemann, F. Hilken, M. Gogolla, R. Wille, Assisted generation of frame conditions for formal models, in Proceedings of the 2015 Design, Automation & Test in Europe Conference & Exhibition, DATE 2015, Grenoble, France, March 9–13, 2015, 2015, pp. 309–312. URL:http://dl.acm.org/citation.cfm?id=2755822
  91. P. Niemann, F. Hilken, M. Gogolla, R. Wille, Extracting frame conditions from operation contracts, in 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MoDELS 2015, Ottawa, ON, Canada, September 30-October 2, 2015, 2015, pp. 266–275. doi:10.1109/MODELS.2015.7338257 Google Scholar
  92. A. Niemetz, M. Preiner, A. Biere, Boolector 2.0. J. Satisfiability, Boolean Modeling and Computation 9, 53–58 (2015) Google Scholar
  93. Object Management Group, UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems, June 2, 2011. 754 pp. Google Scholar
  94. Object Management Group, Object Constraint Language – Version 2.4, Feb 3, 2014. 230 pp. URL:http://www.omg.org/spec/OCL/2.4
  95. Object Management Group, OMG Unified Modeling Language TM (OMG UML) – Version 2.5, Mar 1, 2015. 230 pp. URL:http://www.omg.org/spec/UML/2.5/
  96. J. Peleska, F. Lapschies, H. Löding, P. Smuda, H. Schmid, E. Vorobev, C. Zahlten, Turn Indicator Model Overview. URL:http://www.informatik.uni-bremen.de/agbs/testingbenchmarks/turn_indicator/index_e.html
  97. J. Peleska, Industrial-strength model-based testing - state of the art and current challenges, in Proceedings Eighth Workshop on Model-Based Testing, MBT 2013, Rome, Italy, 17th March 2013, vol. 111. EPTCS, 2013, pp. 3–28. doi:10.4204/EPTCS.111.1 Google Scholar
  98. J. Peters, R. Wille, N. Przigoda, U. Kühne, R. Drechsler, A generic representation of CCSL time constraints for UML/MARTE models, in Proceedings of the 52nd Annual Design Automation Conference San Francisco, CA, USA, June 7–11, 2015, 2015, pp. 122:1–122:6. doi:10.1145/2744769.2744775 Google Scholar
  99. J. Peters, N. Przigoda, R. Wille, R. Drechsler, Clocks vs. instants relations: verifying CCSL time constraints in UML/MARTE models, in 2016 ACM/IEEE International Con- ference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, November 18–20, 2016, 2016, pp. 78–84. doi:10.1109/MEMCOD.2016.7797750 Google Scholar
  100. N. Przigoda, C. Hilken, R. Wille, J. Peleska, R. Drechsler, Checking concurrent behavior in UML/OCL models, in 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MoDELS 2015, Ottawa, ON, Canada, September 30–October 2, 2015, 2015, pp. 176–185. doi:10 1109/MODELS.2015.7338248 Google Scholar
  101. N. Przigoda, J. Peters, M. Soeken, R. Wille, R. Drechsler, Towards an automatic approach for restricting UML/OCL invariability clauses, in Proceedings of the 12th Workshop on Model-Driven Engineering Verification and Validation co- located with ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems, MoDeVVa@MoDELS 2015, Ottawa, Canada, September 29, 2015, vol. 1514. CEUR Workshop Proceedings, 2015, pp. 44–47. URL:http://ceur-ws.org/Vol1514/paper6.pdf
  102. N. Przigoda, J. Stoppe, J. Seiter, R. Wille, R. Drechsler, Verification-driven design across abstraction levels: A case study, in 2015 Euromicro Conference on Digital System Design, DSD 2015, Madeira, Portugal, August 26–28, 2015, 2015, pp. 375–382. doi:10.1109/DSD.2015.88 Google Scholar
  103. N. Przigoda, J.G. Filho, P. Niemann, R. Wille, R. Drechsler, Frame conditions in symbolic representations of UML/OCL models, in 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, November 18–20, 2016, 2016, pp. 65–70. doi:10.1109/MEMCOD.2016.7797747 Google Scholar
  104. N. Przigoda, F. Hilken, J. Peters, R. Wille, M. Gogolla, R. Drechsler, Integrating an SMT-based modelFinder into USE, in Proceedings of the 13th Workshop on Model-Driven Engineering Verification and Validation, co-located with ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems (MODELS 2016), Saint-Malo, France, October 3, 2016, vol. 1713. CEUR Workshop Proceedings, 2016, pp. 40–45. URL:http://ceur-ws.org/Vol-1713/MoDeVVa2016_paper_5.pdf
  105. N. Przigoda, M. Soeken, R. Wille, R. Drechsler, Verifying the structure and behavior in UML/OCL models using satisfiability solvers. IET Cyper-Phys. Syst. Theory Appl. 1(1), 49–59 (2016). doi:10.1049/iet-cps.2016.0022 Google Scholar
  106. N. Przigoda, P. Niemann, J. Peters, F. Hilken, R. Wille, R. Drechsler, More than true or false: native support of irregular values in the automatic validation & verification of UML/OCL models, in Proceedings of the 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2017, Vienna, Austria, September 29–October 02, 2017, 2017, pp. 77–86. doi:10.1145/3127041.3127053 Google Scholar
  107. J. Peters, R. Wille, R. Drechsler, Generating SystemC implementations for clock constraints specified in UML/MARTE CCSL, in 2014 19th International Conference on Engineering of Complex Computer Systems, Tianjin, China, August 4–7, 2014, 2014, pp. 116–125. doi:10.1109/ICECCS.2014.24 Google Scholar
  108. N. Przigoda, R. Wille, R. Drechsler, Contradiction analysis for inconsistent formal models, in 18th IEEE International Symposium on Design and Diagnostics of Electronic Circuits & Systems, DDECS 2015, Belgrade Serbia, April 22–24, 2015, 2015, pp. 171–176. doi:10.1109/DDECS.2015.52 Google Scholar
  109. N. Przigoda, R. Wille, R. Drechsler, Leveraging the analysis for invariant independence in formal system models, in 2015 Euromicro Conference on Digital System Design, DSD 2015, Madeira, Portugal, August 26–28, 2015, 2015, pp. 359–366. doi:10.1109/DSD.2015.85 Google Scholar
  110. N. Przigoda, R. Wille, R. Drechsler, Verbesserung der Fehlersuche in inkonsistenten formalen Modellen (Erweiterte Zusam-menfassung), in Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2015, Chemnitz, Germany, March 3–4, 2015, 2015, pp. 165–172 Google Scholar
  111. N. Przigoda, R. Wille, R. Drechsler, Analyzing inconsistencies in UML/OCL models. J. Circuits Syst. Comput. 25(3) (2016). doi:10.1142/S0218126616400211 Google Scholar
  112. N. Przigoda, R. Wille, R. Drechsler, Ground setting properties for an efficient translation of OCL in SMT-based model finding, in Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems, Saint-Malo, France, October 2–7, 2016, 2016, pp. 261–271. URL:http://dl.acm.org/citation.cfm?id=2976780
  113. A.W. Roscoe, C.A.R. Hoare, R. Bird, The Theory and Practice of Concurrency (Upper Saddle River, NJ, USA, 1997). ISBN:0136744095. URL:https://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf
  114. H. Riener, O. Keszocze, R. Drechsler, G. Fey, A logic for cardinality constraints (extended abstract), in Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, MBMV 2014, Böblingen, Germany, 2014, pp. 217–220 Google Scholar
  115. J.E. Rumbaugh, I. Jacobson, G. Booch, The Unified Modeling Language Reference Manuel - Covers UML 2.0, Second Edition. Addison Wesley Object Technology Series, 2005. ISBN:978-0-321-24562-5 Google Scholar
  116. O. Spinczyk, A. Gal, W. Schröder-Preikschat, AspectC + +: An aspect-oriented extension to the C + + programming language, in International Conference on Tools Pacific: Objects for Internet, Mobile and Embedded Applications, Australian Computer Society, Inc., 2002, pp. 53–60 Google Scholar
  117. K. Sen, D. Marinov, G. Agha, CUTE: a concolic unit testing engine for C, in Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, Lisbon, Portugal, September 5–9, 2005, 2005, pp. 263–272. doi:10.1145/1081706.1081750 Google Scholar
  118. V. Sassone, M. Nielsen, G. Winskel, Models for concurrency: towards a classification. Theor. Comput. Sci. 170(1–2), 297–348 (1996). doi:10.1016/S0304-3975(96)80710-9 ArticleMathSciNetMATHGoogle Scholar
  119. M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla, R. Drechsler, Verifying UML/OCL models using Boolean satisfiability, in Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, March 8–12, 2010, 2010, pp. 1341–1344. doi:10.1109/DATE.2010.5457017 Google Scholar
  120. M. Soeken, Formal specification level: concepts, methods, and algorithms. PhD thesis. University of Bremen, 2013 Google Scholar
  121. M. Sheeran, S. Singh, G. Stålmarck, Checking safety properties using induction and a SAT-Solver, in: Formal Methods in Computer-Aided Design, Third International Conference FMCAD 2000, Austin, Texas, USA, November 1–3, 2000, Proceedings, vol. 1954. Lecture Notes in Computer Science, 2000, pp. 108–125. doi:10.1007/3-540-40922-X_8 Google Scholar
  122. T.S. Staines, Intuitive mapping of UML 2 activity diagrams into fundamental modeling concept Petri Net Diagrams and Colored Petri Nets, in 15th Annual IEEE International Conference and Workshop on Engineering of Computer Based Systems (ECBS 2008), 31 March–4 April 2008, Belfast, Northern Ireland, 2008, pp. 191–200. doi:10.1109/ECBS.2008.12 Google Scholar
  123. D. Steinberg, F. Budinsky, M. Paternostro, E. Merks, EMF: Eclipse Modeling Framework 2.0, 2009 Google Scholar
  124. M. Soeken, R. Wille, R. Drechsler, Encoding OCL data types for SAT-based verification of UML/OCL models, in Tests and Proofs - 5th International Conference, TAP 2011, Zurich,Switzerland, June 30–July 1, 2011, Proceedings, vol. 6706. Lecture Notes in Computer Science, 2011, pp. 152–170. doi:10.1007/978-3-642-21768-5_12 Google Scholar
  125. M. Soeken, R. Wille, R. Drechsler, Towards automatic determination of problem bounds for object instantiation in static model verification, in Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation, 2011, pp. 2:1–2:4 Google Scholar
  126. M. Soeken, R. Wille, R. Drechsler, Verifying dynamic aspects of UML models, in Design, Automation and Test in Europe DATE 2011, Grenoble France March 14–18, 2011, 2011, pp. 1077–1082. doi:10.1109/DATE.2011.5763177 Google Scholar
  127. J. Stoppe, R. Wille, R. Drechsler, Data extraction from SystemC designs using debug symbols and the SystemC API, in IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2013, Natal, Brazil, August 5–7, 2013, 2013, pp. 26–31. doi:10.1109/ISVLSI.2013.6654618 Google Scholar
  128. J. Stoppe, R. Wille, R. Drechsler, Validating SystemC implementations against their formal specifications, in Proceedings of the 27th Symposium on Integrated Circuits and Systems Design, Aracaju, Brazil, September 1–5, 2014, 2014, pp. 13:1–13:8. doi:10.1145/2660540.2660981 Google Scholar
  129. J. Stoppe, R. Wille, R. Drechsler, Automated feature localization for dynamically generated SystemC designs, in Proceedings of the 2015 Design, Automation & Test in Europe Confer ence & Exhibition, DATE 2015, Grenoble France, March 9–13, 2015, 2015, pp. 277–280. URL:http://dl.acm.org/citation.cfm?id=2755814
  130. J. Suryadevara, L. Yin, Timed automata modeling of CCSL constraints, in Formal Techniques for Safety-Critical Systems - First International Workshop, FTSCS 2012, Kyoto, Japan, November 12, 2012, 2012, pp. 152–156. URL:http://csaba.olveczky.se/ftscs12-preproceedings.pdf
  131. E. Torlak, F. Sheng-Ho Chang, D. Jackson, Finding minimal unsatisfiable cores of declarative specifications, in FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26–30, 2008, Proceedings, vol. 5014. Lecture Notes in Computer Science, 2008, pp. 326–341. doi:10.1007/978-3-540-68237-0_23 Google Scholar
  132. E. Torlak, D. Jackson, Kodkod: A relational model finder, in Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 April 1, 2007, Proceedings, vol. 4424. Lecture Notes in Computer Science, 2007, pp. 632–647. doi:10.1007/978-3-540-71209-1_49 Google Scholar
  133. R. Wille, M. Gogolla, M. Soeken, M. Kuhlmann, R. Drechsler, Towards a generic verification methodology for system models, in Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18–22, 2013, 2013, pp. 1193–1196. doi:10.7873/DATE.2013.248 Google Scholar
  134. G. Winskel, M. Nielsen, Models for Concurrency. Tech. rep. 463, 1993 Google Scholar
  135. R. Wille, M. Soeken, R. Drechsler, Debugging of inconsistent UML/OCL models, in 2012 Design, Automation & Test in Europe Conference & Exhibition, DATE 2012, Dresden, Germany, March 12–16, 2012, 2012, pp. 1078–1083. doi:10.1109/DATE.2012.6176655 Google Scholar
  136. L. Yin, F. Mallet, J. Liu, Verification of MARTE/CCSL time requirements in Promela/SPIN, in 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27–29 April 2011, pp. 65–74. doi:10.1109/ICECCS.2011.14 Google Scholar
  137. J. Zhang, S. Shen, J. Zhang, W. Xu, S. Li, Extracting minimal unsatisfiable subformulas in satisfiability modulo theories. Comput. Sci. Inf. Syst. 8(3), 693–710 (2011). doi:10.2298/CSIS101019024Z ArticleGoogle Scholar

Author information

Authors and Affiliations

  1. Mobility Division, Siemens AG, Braunschweig, Germany Nils Przigoda
  2. Johannes Kepler University Linz, Linz, Austria Robert Wille
  3. University of Bremen, Bremen, Germany Judith Przigoda
  4. AG Rechnerarchitektur, University of Bremen, Bremen, Germany Rolf Drechsler
  5. Cyber-Physical Systems, DFKI GmbH, Bremen, Germany Rolf Drechsler
  1. Nils Przigoda
You can also search for this author in PubMed Google Scholar You can also search for this author in PubMed Google Scholar You can also search for this author in PubMed Google Scholar You can also search for this author in PubMed Google Scholar

Rights and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Cite this chapter

Przigoda, N., Wille, R., Przigoda, J., Drechsler, R. (2018). A Symbolic Formulation for Models. In: Automated Validation & Verification of UML/OCL Models Using Satisfiability Solvers. Springer, Cham. https://doi.org/10.1007/978-3-319-72814-8_3

Download citation

Share this chapter

Anyone you share the following link with will be able to read this content:

Get shareable link

Sorry, a shareable link is not currently available for this article.

Copy to clipboard

Provided by the Springer Nature SharedIt content-sharing initiative