Reachability Verification of Rhapsody Statecharts

We present the first fully automated approach for the verification of Rhapsody statecharts. IBM´s Rhapsody framework is widely used in the automotive industry to model embedded reactive systems. The reactive behavior is specified using Rhapsody´s statechart formalism and controls the entire system. Hence, it is crucial to ensure the safety properties of statecharts. Therefore, we constructed a model-checking based approach to verify state reachability, a fundamental safety property, of Rhapsody statecharts. We implemented it in a prototype tool using the model checkers CBMC and SPIN. This tool successfully verified simple models, but failed to scale to industry models due to the sheer complexity of the models. We then designed and implemented a simulation based approach. This successfully verified the simple models and the industry models, and found a crucial bug in one of the industry models. In this paper, we share both our model-checking and simulation approaches, their implementation details and the experimental results.