Abstract
Numerous research projects are done in academia as well as in industry aimed to support the design process based on UML and Model Driven Architecture with new methods and tools that would help to verify both static and dynamic aspects of UML model, to generate the code from it etc. Much attention is paid to the verification of system’s behavior by model checking. In a research project done in the Institute of Computer Science, Warsaw University of Technology, an own model checking environment COSMA is used for these purposes. The approach is based on Concurrent State Machines (CSM), a finite state model well-suited to the representation of systems of concurrent, communicating components. In the paper, the representation of UML state diagrams in terms of CSM is explained and illustrated with an example.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Unified Modeling Language: www.omg.org/technology/documeiits/formal/uml.htm
B. P. Douglass: Advances in the UML for Real-Time Systems, The Addison-Wesley object technology series, 2004.
B. Berard (ed.) et al: Systems and Software Verification: Model-Checking Techniques and Tools, Springer Verlag, 2001
E. M. Clarke, O. Grumberg, D. A. Peled: Model Checking, MIT Press, 2000.
SPIN: http://spinroot.com/spin/
SMV: http://www-2.cs.cmu.edu/modelcheck/smv.html
FormalCheck: www.cadence.com/datasheets/formalcheck.html
Uppaal: http://www.uppaal.com/
Kronos: http://www-verimag.imag.fr/TEMPORISE/kronos/
M. Gallardo, P. Merino, E. Pimentelis: Debugging UML Designs with Model Checking, Journal of Object Technology, vol. 1, no. 2, July–August 2002, pp. 101–117.
J. Lilius and I. Paltor. vUML: A tool for verifying UML models. In Proceedings of 14th IEEE International Conference on Automated Software Engineering, IEEE Press, 1999.
T. Schafer, A. Knapp, S. Merz. Model checking UML state machines and collaborations. Electronic Notes in Theoretical Computer Science, 55(3), 2001.
A. Knapp, S. Merz, Ch. Rauh, Model Checking Timed UML State Machines and Collaborations, W. Damm and E.-R. Olderog (Eds.): FTRTFT 2002, LNCS 2469, pp. 395–414, Springer-Verlag, 2002.
Project Hugo: http://www.pst.informatik.uni-muenchen.de/projekte/hugo/
COSMA: www.ii.pw.edu.pl/cosma/
J. Miescicki: Concurrent State Machines, the formal framework for model-checkable systems, ICS Research Report, 5/2003
J. Miescicki, B. Czejdo, W, B. Daszczuk: Multi-phase model checking in the COSMA environment as a support for the design of pipelined processing. Proc. European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyväskylä, Finland, 24–28 July 2004.
W. B. Daszczuk: Temporal model checking in the COSMA environment (the operation of TempoRG program). ICS Research Report, 7/2003, Warszawa, 2003.
A. Krystosik: ECSM-Extended Concurrent State Machines. ICS Research Report 2/2003
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 International Federation for Information Processing
About this paper
Cite this paper
Mieścicki, J. (2006). Verification of UML State Diagrams Using Concurrent State Machines. In: Sacha, K. (eds) Software Engineering Techniques: Design for Quality. IFIP International Federation for Information Processing, vol 227. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-39388-9_25
Download citation
DOI: https://doi.org/10.1007/978-0-387-39388-9_25
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-39387-2
Online ISBN: 978-0-387-39388-9
eBook Packages: Computer ScienceComputer Science (R0)