Verifying Statemate Statecharts Using CSP and FDR

  • A. W. Roscoe
  • Z. Wu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)


We propose a framework for the verification of statecharts. We use the CSP/FDR framework to model complex systems designed in statecharts, and check for system consistency or verify special properties within the specification. We have developed an automated translation from statecharts into CSP and exploited it in both theoretical and practical senses.


State Machine Sequential Machine Race Condition Symbolic Model Check Statechart Diagram 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Anderson, R., Beame, P., Burns, S., Chan, W., Modugno, F., Notkin, D., Reese, J.: Model checking large software specifications. IEEE Transactions on Software Engineering 24(7), 498–520 (1998)CrossRefGoogle Scholar
  2. 2.
    Bienmuller, T., Bohn, J., Brinkmann, H., Brockmeyer, U., Damm, W., Hungar, H., Jansen, P.: Verification of automotive control units. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol. 1710, pp. 319–341. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bienmuller, T., Brockmeyer, U., Damm, W., Dohmen, G., Holberg, H.-J., Hungar, H., Josko, B., Schlor, R., Wittich, G., Wittke, H., Clements, G., Rowlands, J., Sefton, E.: Formal verification of an avionics application using abstraction and symbolic model checking. In: Redmill, F., Anderson, T. (eds.) Towards System Safety - Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK. Safety-critical Systems Club, pp. 150–173. Springer, Berlin (1999)Google Scholar
  4. 4.
    Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991, Edinburgn, Scotland (1990)Google Scholar
  5. 5.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: 27th ACM/IEEE Design Automation Conference (1990)Google Scholar
  6. 6.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 10E20 states and beyond. In: LICS (1990)Google Scholar
  7. 7.
    Bienmuller, T., Damm, W., Wittke, H.: The Statemeat Verification Environment – Making it real. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, p. 561. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. In: Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages (1992)Google Scholar
  9. 9.
    Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. In: FMOODS 1999 IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems. Kluwer Academic Publishers, NY (1999)Google Scholar
  10. 10.
    Damm, W., Josko, B., Hungar, H., Pnueli, A.: A compositiona real-time semantics of STATEMATE designs. In: de Roever, W.-P. (ed.) Proceedings, International Symposium on Compositionality-The Significant Diference. LNCS. Springer, Heidelberg (1998)Google Scholar
  11. 11.
    Damm, W., Klose, J.: Verification of a radio-based signalling system using the Statemate verification environment. Formal Methods in System Design 19, 121–141 (2001)zbMATHCrossRefGoogle Scholar
  12. 12.
    Eshuis, H., Wieringa, R.: A Formal Semantics for UML Activity Diagrams C Formalising Workflow Models, Technical Report (2001)Google Scholar
  13. 13.
    Formal Systems (Europe) Ltd., Failures-Divergence Refinement, User Manual, obtainable from:
  14. 14.
    Fuhrmann, K., Hiemer, J.: Formal Verification of STATEMATE-Statecharts (2001),
  15. 15.
    Fokkink, W.J., Hollingshead, P.: Verification of interlockings: from control tables to ladder logic diagrams. In: Proceedings of the 3rd Workshop on Formal Methods for Industrial Critical Systems-FMICS 1998, Amsterdam, Stichting Mathematisch Centrum (1998)Google Scholar
  16. 16.
    Feyerabend, K., Josko, B.: VIS: A visual formalism for real time requirement specifications. In: Rus, T., Bertrán, M. (eds.) AMAST-ARTS 1997, ARTS 1997, and AMAST-WS 1997. LNCS, vol. 1231, pp. 156–168. Springer, Heidelberg (1997)Google Scholar
  17. 17.
    Group, T.V.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)Google Scholar
  18. 18.
    Harel, D., Naamad, A.: The Statemate Semantics of Statecharts, Technical Report, i-Logix (1995)Google Scholar
  19. 19.
    Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Trauring, A.S.: Statemate: A Working Environment for the Development of Complex Reactive Systems. IEEE Transactions on Software Engineering 16(4) (1990)Google Scholar
  20. 20.
    Hudak, J., Dorda, S.C., Gluch, D.P., Lewis, G., Weinstock, C.: Model-Based Verification: Abstraction Guidelines, Technical Note CMU/SEI-2002-TN-001 (2002)Google Scholar
  21. 21.
    Harel, D., Politi, M.: Modeling Reactive Systems with Statecharts: The STATEMATE Approach, Part No.D-1100-43, i-Logix Inc., Three Riverside Drive, Andover, MA 01810 (June 1996)Google Scholar
  22. 22.
    The MathWorks, Stateflow, User Manual, obtainable from:
  23. 23.
    Mikk, E., Lakhnech, Y., Petersohn, C., Siegel, M.: On Formal Semantics of Statecharts as Supported by STATEMATE, Technical Report, BCS-FACS Northern Formal Methods Workshop, 2, Ilkley (1997)Google Scholar
  24. 24.
    Moser, L.E., Ramakrishna, Y., Kutty, G., Melliar-Smith, P., Dillon, L.: A graphical environment for design of concurrent real-time systems. ACM Transactions on Software Engineering and Methodology 6(1), 31–79 (1997)CrossRefMathSciNetGoogle Scholar
  25. 25.
    Roscoe, A.W.: The theory and practice of concurrency. Prentice-Hall International, Englewood Cliffs (1998)Google Scholar
  26. 26.
    Roscoe, A.W.: Compiling Statemate Statecharts into CSP and verifying them using FDR – abstract, Technical Report (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • A. W. Roscoe
    • 1
  • Z. Wu
    • 1
  1. 1.Oxford University Computing Laboratory 

Personalised recommendations