Abstract
The symbolic formulation and its extensions introduced in the previous chapters allow to solve various validation and verification problems for UML/OCL models—illustrating the generality of this method. However, the possibilities of such a symbolic representation go far beyond pure functional descriptions. In fact, also non-functional constraints as, e.g., timing issues can be checked with this methodology. This is covered in this chapter. To this end, we consider descriptions provided in MARTE/CCSL. While MARTE/CCSL itself is a profile for the UML, it is not part of classical UML but close enough to easily formulate it in UML. Hence, the first section shows how to obtain such a formalization and, by this, also implementation of MARTE/CCSL using the formalization of UML given before. Afterwards, it is demonstrated how specific verification and validation tasks can be tackled using the features of the formalization of UML/OCL. This leaves the designer with means to formulate most of the properties to be described in UML/OCL to be solved by the method proposed in this book. As both, the problems to be formulated and the solving engine behind are exchangeable with limited effort by the designer this leads to a highly flexible way of solving verification and validation problems during system design.
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.
For the sake of clarity, a precise definition, e.g., of the domain of a variable \(v\in {{\mathcal {V}} }\ \) is omitted here, but will be provided later in Sect. 6.2.1.
- 2.
Note that, in many cases, the number of states to be considered can already be restricted at the very beginning. As an example, it is already obvious from the CCSL constraints in Fig. 6.2a and discussed in Example 46 that only two states are required. However, in order to keep the following descriptions generic, such cases are not explicitly discussed in the following.
- 3.
Note that the evaluation will be false, if one of the index variables remained un-assigned.
- 4.
Note that this does not guarantee the occurrence of a group in an actual system, as this additionally depends on the precise implementation of the system. Nevertheless, this proof shows that the desired timing behavior is, in principle, possible.
- 5.
This has already been identified as bottleneck before in this section.
References
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
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
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
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
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
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
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
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
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
Object Management Group, UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems, June 2, 2011. 754 pp.
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
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
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
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
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
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
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
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). Timing Aspects. In: Automated Validation & Verification of UML/OCL Models Using Satisfiability Solvers. Springer, Cham. https://doi.org/10.1007/978-3-319-72814-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-72814-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72813-1
Online ISBN: 978-3-319-72814-8
eBook Packages: EngineeringEngineering (R0)