Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
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)
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)
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transition relations. In: VLSI 1991, Edinburgn, Scotland (1990)
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)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 10E20 states and beyond. In: LICS (1990)
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)
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)
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)
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)
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)
Eshuis, H., Wieringa, R.: A Formal Semantics for UML Activity Diagrams C Formalising Workflow Models, Technical Report (2001)
Formal Systems (Europe) Ltd., Failures-Divergence Refinement, User Manual, obtainable from: http://www.fsel.com/fdr2_manual.html
Fuhrmann, K., Hiemer, J.: Formal Verification of STATEMATE-Statecharts (2001), Citeseer.nj.nec.com/255163.html
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)
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)
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)
Harel, D., Naamad, A.: The Statemate Semantics of Statecharts, Technical Report, i-Logix (1995)
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)
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)
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)
The MathWorks, Stateflow, User Manual, obtainable from: http://www.mathworks.com/access/helpdesk/help/toolbox/stateflow/ug/
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)
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)
Roscoe, A.W.: The theory and practice of concurrency. Prentice-Hall International, Englewood Cliffs (1998)
Roscoe, A.W.: Compiling Statemate Statecharts into CSP and verifying them using FDR – abstract, Technical Report (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roscoe, A.W., Wu, Z. (2006). Verifying Statemate Statecharts Using CSP and FDR. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_18
Download citation
DOI: https://doi.org/10.1007/11901433_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)