Generacja kodu dla asynchronicznych wywołań funkcji w środowisku COSMA dla modelu CSM/ECSM

• Autorzy: Grabski W. , Nowacki M.

Warianty tytułu

EN

Code generation for the asynchronuos function calls in CSM/ECS model in COSMA environment

• Języki publikacji: PL

Abstrakty

PL

Środowisko COSMA, rozwijane w Instytucie Informatyki Politechniki Warszawskiej, powstało z myślą o weryfikacji modeli (model checking) systemów reaktywnych specyfikowanych przy pomocy automatów CSM (Concur-rent State Machines). ECSM (Extended CSM) stanowi rozszerzenie modelu CSM o złożone struktury danych, atrybuty związane z przejściami i stanami oraz możliwość bezpośredniego użycia kodu w C/C++. Powoduje to, że model wyrażony w ECSM nie może być formalnie weryfikowany, a jedynie stanowić krok pośredni przy generacji kodu. W takim podejściu model CSM reprezentuje sterowanie i komunikację pomiędzy modułami systemu, podczas gdy elementy ECSM, dane i szczegóły przetwarzania. Artykuł omawia sposób modelowania wywołań asynchronicznych w modelu CSM/ECSM i metodę generacji kodu z modelu ECSM zawierającego asynchroniczne wywołania funkcji. Omawiany temat zilustrowany jest przykładem.

EN

The COSMA software environment, developed in the Institute of Computer Science, WUT, was designed primarily for model checking of reactive systems specified in terms of Concurrent State Machines (CSM). However, COSMA supports also Extended CSM (ECSM). The extensions allow for using complex data types and pieces of C/C++ code, attributed to CSM states and/or transitions. Because of these extensions, ECSM models cannot be verified by model checking, but they can be used as an intermediate step in code generation. The underlying CSM represent then the flow of control within cooperating components and the communication among them white the extensions specify the data structures and the details of their processing. The paper discusses modeling the asynchronous function calls in CSM/ECSM diagrams and the code generation from ECSM diagrams which models asynchronous function calls. The approach is illustrated with an example.

Słowa kluczowe

PL

model CSM/ECSM; podstawy generacji kodu; modelowanie wywołań asynchronicznych; metody generacji kodu

EN

CSM/ECS model; modeling the asynchronous function; code generation from ECMS diagrams

• Wydawca: Wydział Elektroniki, Telekomunikacji i Informatyki Politechniki Gdańskiej
• Czasopismo: Zeszyty Naukowe Wydziału ETI Politechniki Gdańskiej. Technologie Informacyjne
• Rocznik: 2007
• Tom: T. 13
• Strony: 339--346
• Opis fizyczny: Bibliogr. 11 poz., rys.

Twórcy

autor

Grabski W.

autor

Nowacki M.

• Instytut Informatyki, Politechnika Warszawska

Bibliografia

• [1] COSMA project: http://www.ii.pw.edu.pl/cosma/
• [2] B. Berard (ed.) et al.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer Verlag, 2001
• [3] E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 2000
• [4] J. Mieścicki: Concurrent State Machines, the formal framework for model-checkable systems, ICS Research Report, 5/2003
• [5] Krystosik: ECSM - Extended Concurrent Stale Machines. ICS Research Report 2/2003
• [6] Unified Modeling Language: http://www.omg.orgltechnology/documents/formal/uml.htm
• [7] W. B. Daszczuk: Temporal model checking in the COSMA environment (the operation of TempoRG program), Institute of Computer Science, WUT, Research Report nr 7/2003
• [8] Knapp, S. Merz: Model Checking and Code Generation for UML Stale Machines and Collaborations, Proc. 5th Tools for System Design and Verification, p. 59-64
• [9] WSGenerator tool: http://www.ii.pw.edu.pl/cosma/code generator/
• [10] K. Łukasiuk: Construction of Internet applications based on client-server architecture using COSMA design environment MSc. diploma ISC, 2006 (in Polish)
• [11] W.Grabski, M.Nowacki: Code Generation For CSM/ECSM Models in COSMA Environment, Proc. of the IMCSIT, Vol. l, XXII Autumn Meeting of Polish Information Processing Society, Wisła, Poland, November, 2006, p. 393-400.