Concurrent systems modeling with CCL

• Autorzy: Kułakowski K.

Warianty tytułu

PL

Modelowanie systemu w CCL

• Języki publikacji: EN

Abstrakty

EN

One of the challenges facing software engineering is to conduct research into new methods of modeling systems. The CCL notation shown in the article tries to follow in this direction. The solutions and methods presented here indicate its practical application to modeling complex eomputer systems using the struetural, dataflowcentric approach. The basis for the proposed integration between CCL and struetural methods is the newly defined externalization mechanism. It allows the details of inter-process communication to be abstracted away, thereby reducing the size of the submodels which are subject to further verification. Thanks to the methods adopted here, the overall picture of the system becomes morę readable for humans, and, due to the significant submodel state space reduction, the effective use of formal methods for their analysis becomes possible.

PL

Jednym z podstawowych zadań związanych z inżynierią oprogramowania jest szukanie nowych i optymalizacja istniejących metod modelowania systemów informatycznych. Przedstawiona w pracy notacja CCL stara się wpisywać w ten nurt badań. Prezentowane podejście pokazuje jej użyteczność w kontekście użycia metod strukturalnych (diagramy przepływu danych) do modelowania złożonych systemów informatycznych. Podstawą proponowanej integracji pomiędzy CCL i metodami modelowania strukturalnego jest nowowprowadzone pojęcie eksternalizacji. Pozwala ono abstrahować od szczegółów implementacyjnych komunikacji międzyprocesowej, redukując tym samym wielkość modeli podlegających dalszej weryfikacji. Dzięki przyjętemu rozwiązaniu modele stają się bardziej czytelne dla projektantów, oraz dzięki znaczącej redukcji przestrzeni stanów, możliwe staje się efektywne wykorzystanie metod formalnych w celu ich dalszej analizy.

Słowa kluczowe

EN

CCL; DFD; software engineering; formal methods; state explosion problem

PL

CCL; DFD; inżynieria oprogramowania; metody formalne; eksplozja stanów

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Automatics
• Rocznik: 2012
• Tom: Vol. 16, no. 2
• Strony: 115--125
• Opis fizyczny: Bibliogr. 15 poz., rys., tab.

Twórcy

autor

Kułakowski K.

• AGH University of Science and Technology, Institute of Applied Computer Science

Bibliografia

• [1] Aldini A. et al., A process algebraic approach to software architecture design. sti.nniurb.it, Berlin, Heidelberg, 2009.
• [2] Baier C. et al., Principles of Model Checking. mitpress.mit.edu, 2008.
• [3] Barbosa P. et al., Checking Semantics Equivalence of MDA Transformations in Concurrent Systems. J Univers Comput Sci., 15, 11, 2009, 2196-2224.
• [4] Bergstra J.A. et al., eds: Handbook of Process Algebra. Elsevier Science, 2001.
• [5] Fencott C, Formal methods for concurrency. International Thomson Computer Press, 1996.
• [6] Garavel H. et al., Cadp 2010: A toolbox for the construction and analysis of distributed processes. Tools and Algorithms for the Construction and Analysis of Systems - TAC AS, 2011.
• [7] Graham P., ANSI Common Lisp. Prentice Hali, 1995.
• [8] Holzmann G., Smith M., Automating software feature verification. Bell Labs Tech J., 5, 2, 2000, 72-87.
• [9] Karvi T. et al., Stepwise Development of Process-Algebraic Specifications in Decorated Trace Semantics. Form Method Syst Des., 26, 3, 2005, 293-317.
• [10] Kułakowski K., CCL Sim, the simulation environment for concurrent systems. To be appeard in Proceedings of Dependability and Complex Systems DepCoS-RELCOMEX, 2012.
• [11] Kułakowski K., Szmuc T., Concurrent Communicating Lists — executable modeling library. Submitted to Journal of Functional Programming, 2012, 1-43.
• [12] Milner R., A calculus of communicating systems. 1982.
• [13] VanderHart L., Sierra S., Practical Clojure. Apress, 2009.
• [14] Wirth N., Program development by stepwise refinement.
• [15] Yourdon E., Modern structured analysis. Prentice Hall, 1989.