Code generation for CSM/ECSM models in COSMA environment

• Autorzy: Grabski W. , Nowacki M.

Warianty tytułu

PL

Generacja kodu programu na podstawie modelu CSM/ECSM w środowisku COSMA

• Języki publikacji: EN

Abstrakty

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 verifed 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 while the extensions specify the data structures and the details of their processing. The paper discusses the code generation from ECSM diagrams. The approach is illustrated with an example.

PL

Środowisko COSMA, rozwijane w Instutycie Informatyki Politechniki Warszawskiej, powstało z myślą o weryfikacji modeli (model checking) systemów reaktywnych specyfikowanych przy pomocy automatów CSM (Concurrent State Machines) jak i ich rozszerzonej wersji (ECSM - Extended CSM). Rozszerzenie CSM o złożone struktury danych, atrybuty związane z przejściami i stanami oraz możliwość bezpośredniego użycia kody w C/C++ powodują, ż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 ECSM - dane i szczegóły przetwarzania. Artykuł omawia generację kodu z modelu ECSM zilustrowaną przykładem.

Słowa kluczowe

EN

model checking; COSMA; code generation; CSM; ECSM; FSM

PL

weryfikacja; COSMA; generacja kodu; CSM; ECSM; automat skończenie stanowy

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2007
• Tom: Vol. 8, Spec. Ed
• Strony: 49--59
• Opis fizyczny: Bibliogr. 10 poz., rys.

Twórcy

autor

Grabski W.

• Institute of Computer Science, Warsaw University of Technology, Warszawa, Poland

autor

Nowacki M.

• Institute of Computer Science, Warsaw University of Technology, Warszawa, Poland

Bibliografia

• [1] Unified Modeling Language: http://www.omg.org/techiLOlogy/documents/ formal/uml.htm
• [2] Berard B. (ed.) et al.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer Verlag, 2001
• [3] Clarke E.M., Grumberg O., Peled D. A.: Model Checking, MIT Press, 2000
• [4] Project Hugo: http://www.pst.informatik.uni-muenchen.de/projekte/hugo/
• [5] COSMA project: http://www.ii.pw.edu.pl/cosma/
• [6] Mieścicki J.: Concurrent StateMachines, the formal framework for model-checkable systems, ICS Research Report 5/2003
• [7] Krystosik A.: ECSM — Extended Concurrent State Machines. ICS Research Report 2/2003
• [8] WSGenerator tool: http://www. ii.pw.edu.pl/cosma/code_generator/
• [9] Łukasiuk K.: Construction of Internet applications based on client—server archi-tecture using COSMA design environment. M.Sc. diploma ISC, 2006 (in Polish)
• [10] Knapp A., Merz S.: Model Checking and Code Generation for UML State Machines and Collaborations, Proc. 5th Wsh. Tools for System Design and Verification 2002, p. 59-64