Powiadomienia systemowe
- Sesja wygasła!
- Sesja wygasła!
Tytuł artykułu
Treść / Zawartość
Pełne teksty:
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
This paper proposes an approach that integrates UML 2.0 Activity Diagrams (UML2-ADs) and the communicating sequential process (CSP) for modeling and verifying software systems. A UML2-AD is used for modeling a software system, while a CSP is used for verification purposes. The proposed approach consists of another way of transforming UML2-AD models to CSP models. It also focuses on checking the correctness of some properties of the transformation itself. These properties are specified using linear temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on model -driven engineering (MDE). The meta-modeling is realized using the AToMPM tool, while the model transformation and the correctness of its properties are realized using the GROOVE tool. Finally, we illustrated this approach through a case study.
Wydawca
Czasopismo
Rocznik
Tom
Strony
209–233
Opis fizyczny
Bibliogr. 27 poz., rys.
Twórcy
autor
- MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria
autor
- MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria
autor
- MISC Laboratory, University Constantine 2 – Abdelhamid Mehri, Algeria
Bibliografia
- [1] Amrani M., Combemale B., L´ucio L., Selim G., Dingel J., Le Traon Y., Vangheluwe H., Cordy J.R.: Formal Verification Techniques for Model Transformations: A Tridimensional Classification, The Journal of Object Technology, vol. 14(3), pp. 1–43, 2015. doi: 10.5381/jot.2015.14.3.a1.
- [2] AToMPM project: 2019. http://www-ens.iro.umontreal.ca/∼syriani/atompm/ atompm.htm.
- [3] Bisztray D., Ehrig K., Heckel R.: Case study: UML to CSP Transformation, 2007. AGTIVE 2007 Tool Contest Overview. https://www.informatik.uni-marburg.de/ ∼swt/agtive-contest/UML-to-CSP.pdf.
- [4] Brenas J.H., Echahed R., Strecker M.: Ensuring Correctness of Model Transformations While Remaining Decidable. In: International Colloquium on Theoretical Aspects of Computing, pp. 315–332, Springer, 2016.
- [5] Busser de J.: Model checking AToMPM transformation systems with GROOVE, Technical report, University of Antwerp, 2015.
- [6] Calegari D., Szasz N.: Verification of Model Transformations: A Survey of the State-of-the-Art, Electronic Notes in Theoretical Computer Science, vol. 292, pp. 5–25, 2013.
- [7] Cuadrado J.S., Guerra E., de Lara J., Claris´o R., Cabot J.: Translating Target to Source Constraints in Model-to-Model Transformations. In: 2017 ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS), pp. 12–22, IEEE, 2017. doi: 10.1109/MODELS.2017.12.
- [8] Ehrig H., Hermann F., Sartorius C.: Completeness and Correctness of Model Transformations Based on Triple Graph Grammars With Negative Application Conditions, Electronic Communications of the EASST, vol. 18, 2009.
- [9] Ghamarian A.H., Mol de M., Rensink A., Zambon E., Zimakova M.: Modelling and analysis using GROOVE, International Journal on Software Tools for Technology Transfer, vol. 14(1), pp. 15–40, 2012. doi: 10.1007/s10009-011-0186-x.
- [10] Gogolla M., Hamann L., Hilken F.: Checking Transformation Model Properties with a UML and OCL Model Validator. In: Proceedings of 3rd International Workshop on Verification of Model Transformation (VOLT’2014), pp. 16–25, 2014.
- [11] GROOVE Home Page: 2019. http://GROOVE.cs.utwente.nl/.
- [12] Guerra E., Lara de J., Wimmer M., Kappel G., Kusel A., Retschitzegger W., Schonbock J., Schwinger W.: Automated verification of model transformations based on visual contracts, Automated Software Engineering, vol. 20, pp. 5–46, 2013. doi: 10.1007/s10515-012-0102-y.
- [13] Hoare C.A.R.: Communicating sequential processes, Communications of the ACM, vol. 21(8), pp. 666–677, 1978. doi: 10.1145/359576.359585.
- [14] Lengyel L., Charaf H.: Test-driven verification/validation of model transformations, Frontiers of Information Technology & Electronic Engineering, vol. 16(2), pp. 85–97, 2015.
- [15] Lucio L., Amrani M., Dingel J., Lambers L., Salay R., Selim G.M., Syriani E., Wimmer M.: Model transformation intents and their properties, Software & Systems Modeling, vol. 15(3), pp. 647–684, 2016.
- [16] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: Transformation and validation of BPMN models to Petri nets models using GROOVE. In: 2016 International Conference on Advanced Aspects of Software Engineering (ICAASE), pp. 22–29, IEEE, 2016.
- [17] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL. In: 2017 IEEE International Conference on Information Reuse and Integration (IRI), pp. 419–426, IEEE, 2017.
- [18] Meghzili S., Chaoui A., Strecker M., Kerkouche E.: Verification of Model Transformations Using Isabelle/HOL and Scala, Information Systems Frontiers, vol. 21(1), pp. 45–65, 2019.
- [19] Penker M.: Business Modeling With UML: Business Patterns at Work, John Wiley & Sons, 2000.
- [20] Putter de S., Wijs A.: A formal verification technique for behavioural model-to-model transformations, Formal Aspects of Computing, vol. 30(1), pp. 3–43, 2018. doi: 10.1007/s00165-017-0437-z.
- [21] Rahim L.A., Whittle J.: A survey of approaches for verifying model transformations, Software & Systems Modeling, vol. 14(2), pp. 1003–1028, 2015.
- [22] Rensink A.: The GROOVE Simulator: A Tool for State Space Generation. In: International Workshop on Applications of Graph Transformations with Industrial Relevance, pp. 479–485, Springer, 2003. doi: 10.1007/978-3-540-25959-6 40.
- [23] Rozenberg G.: Handbook of Graph Grammars and Computing by Graph Transformation. Volume 1: Foundations, World Scientific, 1997. doi: 10.1142/3303.
- [24] Schurr A.: Specification of Graph Translators With Triple Graph Grammars. In: International Workshop on Graph-Theoretic Concepts in Computer Science, pp. 151–163, Springer, 1994.
- [25] Silva da A.R.: Model-driven engineering: A survey supported by the unified conceptual model, Computer Languages, Systems & Structures, vol. 43, pp. 139–155, 2015. doi: 10.1016/j.cl.2015.06.001.
- [26] UML diagrams: Process Shopping Order. UML Activity Diagram Example: 2015. https://www.uml-diagrams.org/shopping-process-order-uml-activitydiagram-example.html?context=activity-examples.
- [27] Unified Modeling Language Specification, version 2.0: 2005. https://www.omg. org/spec/UML/2.0/About-UML/.
Uwagi
PL
„Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).”
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-bd81a677-9051-43b8-93bf-f9078109e6db