Ś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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.