Abstract
The formalization and actual implementation of UML/OCL offers great opportunities for analyzing and solving verification and validation problems during system design. Moreover, the solutions for this purpose introduced in the previous chapters are rather generic and can not only be applied for structural and behavioral descriptions but also extended, e.g., for timing issues. In this chapter, we further extend this generality. We observe thereby that for other problems often formulations result which are rather huge—although often much more compact representations are possible. To this end, we describe the concept of ground setting properties which allows to represent a problem in a much more compact fashion—significantly increasing the performance of the solving process.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Note that Player B wins, if the game starts on field (1,1), since Player A has to make the first move but no valid options to do so.
- 2.
Note that, in Listing 7.2, unsigned bit vectors have been used and, thus, the comparison looks a bit different as in the corresponding OCL constraints.
- 3.
The files of the resulting SMT formulations are online available: http://informatik.uni-bremen.de/agra/divers/gsp/.
- 4.
Note that false is assumed as default value.
- 5.
Since the USE model validator does not provide any information on the size of the resulting SAT instance, only SMT-based model finding is considered in this part of the evaluation.
- 6.
Note that, without calculating the size of the SMT instance, the general SMT-based model finder was capable of determining solutions for 5 × 5 and 6 × 6 as well (but approached its limits for problems sizes of 7 × 7 or larger).
References
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
D. Jackson, Software Abstractions - Logic, Language, and Analysis, 2012, pp. I–XVI, 1–350. ISBN: 978-0-262-10114-1
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
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
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
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
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
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
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
Author information
Authors and Affiliations
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). Reducing Instance Sizes with Ground Setting Properties. In: Automated Validation & Verification of UML/OCL Models Using Satisfiability Solvers. Springer, Cham. https://doi.org/10.1007/978-3-319-72814-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-72814-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72813-1
Online ISBN: 978-3-319-72814-8
eBook Packages: EngineeringEngineering (R0)