CODE GENERATION FOR CSM/ECSM MODELS IN COSMA ENVIRONMENT
DOI:
https://doi.org/10.7494/csci.2007.8.3.49Keywords:
Model Checking, COSMA, Code Generation, CSM, ECSM, FSMAbstract
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.Downloads
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
