CODE GENERATION FOR CSM/ECSM MODELS IN COSMA ENVIRONMENT

Waldemar Grabski, Michał Nowacki

Abstract


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 ConcurrentState Machines (CSM). However, COSMA supports also Extended CSM (ECSM).The extensions allow for using complex data types and pieces of C/C++ code, attributedto CSM states and/or transitions. Because of these extensions, ECSM models cannot beverified 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 andthe communication among them while the extensions specify the data structures and thedetails of their processing.The paper discusses the code generation from ECSM diagrams. The approach is illustratedwith an example.

Keywords


Model Checking; COSMA; Code Generation; CSM; ECSM; FSM

Full Text:

PDF

References


Unified Modeling Language: http://www.omg.org/technology/documents/formal/uml.htm

Berard B. (ed.) et al.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer Verlag, 2001

Clarke E.M., Grumberg O., Peled D.A.: Model Checking, MIT Press, 2000

Project Hugo: http://www.pst.informatik.uni-muenchen.de/projekte/hugo/

COSMA project: http://www.ii.pw.edu.pl/cosma/

Mieścicki J.: Concurrent StateMachines, the formal framework for modelcheckable systems, ICS Research Report 5/2003

Krystosik A.: ECSM — Extended Concurrent State Machines. ICS Research Report 2/2003

WSGenerator tool: http://www.ii.pw.edu.pl/cosma/code_generator/

Łukasiuk K.: Construction of Internet applications based on client—server architecture using COSMA design environment. M.Sc. diploma ISC, 2006 (in Polish)

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




DOI: https://doi.org/10.7494/csci.2007.8.3.49

Refbacks

  • There are currently no refbacks.