Formal Analysis of Service-oriented Architectures

• Autorzy: Rafe V.

Warianty tytułu

PL

Analiza formalna architektury typu service-oriented

• Języki publikacji: EN

Abstrakty

EN

Even though model checking is one of the most accurate analyses techniques to verify software systems, the problem of model checking is that it is not feasible for large and complex software systems, which their state spaces are too large. In these situations one can use scenariobased model checking techniques. In this paper, we present an approach to analyze large and complex systems specified by graph transformation systems. To do so, we propose the scenario-based model checking techniques. We explain how the approach will affect to the size of the state space by focusing on the most important occurring scenarios in a system.

PL

Problem sprawdzania modelu software jest istotny jeśli badamy duży i złożony system. W artykule zaprezentowano metodę umożliwiającą taką analizę systemu opisanego przez transformację grafu. Zaproponowano technikę sprawdzania opierającą się na modelu bazującym na scenariuszu.

Słowa kluczowe

EN

graph transformation; SOA; verification; Bogor; electrical technology; electrical power engineering

PL

software; transformacja grafu; elektrotechnika; elektroenergetyka

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2011
• Tom: R. 87, nr 11
• Strony: 310--313
• Opis fizyczny: Bibliogr. 19 poz., il., tabl., wykr.

Twórcy

autor

Rafe V.

• Department of Computer Engineering, Faculty of Engineering, Arak University, Arak 38156-8-8349, Iran,

Bibliografia

• [1] C. Baier and J.P. Katoen. Principals of Model Checking. The MIT Press, (2008)
• [2] L. Baresi, R. Heckel, S. Thöne, and D. Varró. Modeling and validation of service-oriented architectures: Application vs. style. In Proc. ESEC/FSE 03 European Software Engineering Conference and ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 68–77. ACM Press, (2003)
• [3] L. Baresi, R. Heckel. Tutorial introduction to graph transformation: a software engineering perspective. Proc. First Int. Conf. Graph Transformation (ICGT), (LNCS, 2505), pp. 402–429, (2002)
• [4] H. Ehrig, K. Ehrig, U. Prange and G. Taentzer: Fundamentals of Algebraic Graph Transformations, Springer, (2006)
• [5] A. Rensink. The GROOVE Simulator: A Tool for State Space Generation, In Applications of Graph Transformations with Industrial Relevance (AGTIVE), vol. 3062 of Lecture Notes in Computer Science, 479–485, (2004)
• [6] L. Baresi, V. Rafe, A. T. Rahmani and P. Spoletini: “An Efficient Solution for Model Checking Graph Transformation Systems”, Electronic Notes in Theoretical Computer Science (ENTCS), Vol. 213, Elsevier Science B.V., ISSN: 1571-0661, PP. 3-21 (2008)
• [7] A. Schmidt and D. Varró, CheckVML: A Tool for Model Checking Visual Modeling Languages, In Proc. of 6th International Conference on the Unified Modeling Language (UML), vol. 2863 of LNCS, 92–95, (2003)
• [8] L. Baresi, R. Heckel, S. Thöne, and D. Varró. Style-based modeling and refinement of service-oriented architectures. Int. Journal on Software and Systems Modeling, SoSyM, (2006)
• [9] V. Rafe, A. T. Rahmani, L. Baresi, P. Spoletini: “Towards Automated Verification of Layered Graph Transformation Specifications”, journal of IET Software, Vol.3 No.4, pp. 276- 291 (2009).
• [10] Robby, M. Dwyer, and J. Hatcliff. Bogor: An Extensible and Highly-Modular Software Model Checking Framework, In Proc. of the 9th European software engineering Confference, 267– 276, (2003)
• [11] Object Management Group. UML specification version 1.4, (2001). http://www.omg.org/uml/.
• [12] L. Baresi, R. Heckel, S. Thöne, and D. Varró. Style-based refinement of dynamic software architectures. In Proc. of the 4th Working IEEE/IFIP Conference on Software Architecture, WICSA 2004, pages 155–164. IEEE Computer Society, (2004)
• [13] L. Baresi, R. Heckel, S. Thöne, and D. Varró. Modeling and analysis of architectural styles based on graph transformation. In Proc. 6th ICSE Workshop on Component-Based Software Engineering (CBSE6): Automated Reasoning and Prediction, pages 67–72, (2003)
• [14] The Mur?. Model Checker: http://verify.stanford.edu/dill/murphi.html
• [15] Rensink A., Schmidt A´ ., Varro D.: ‘Model checking graph transformations: a comparison of two approaches’. Proc. Second Int. Conf. Graph Transformation (ICGT), (LNCS, 3256), pp. 226–241, (2004)
• [16] J. Lilius and I.P. Paltor. vUML: a tool for verifying UML models. In Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE), pages 255–258, (1999)
• [17] K. Compton, Y. Gurevich, J. Huggins, and W. Shen. An automatic verification tool for UML. Technical Report CSE-TR- 423-00, University of Michigan, EECS Department, (2000)
• [18] S. Gnesi, D. Latella, and M. Massink. Model checking UML statecharts diagrams using JACK. In Proceedings of the 4th IEEE International Symposium on High Assuarance Systems Enginering (HASE), pages 46–55. IEEE Press, (1999)
• [19] T. Schäfer, A. Knapp, and S. Merz. Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science, 55(3):13 pages, (2001)