Skip to main content

Verifying Statemate Statecharts Using CSP and FDR

A. W. Roscoe and Zhenzhong Wu


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.

Book Title
Proceedings of ICFEM 2006