Refinement of Statecharts with Run-to-Completion Semantics

Abstract

Statechart modelling notations, with so-called ‘run to completion’ semantics and simulation tools for validation, are popular with engineers for designing systems. However, they do not support formal refinement and they lack formal static verification methods and tools. For example, properties concerning the synchronisation between different parts of a system may be difficult to verify for all scenarios, and impossible to verify at an abstract level before the full details of substates have been added. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible, restricting instantiation and testing to a validation role. In this paper, we introduce a notion of refinement, similar to that of Event-B, into a ‘run to completion’ Statechart modelling notation, and leverage Event-B’s tool support for proof. We describe the pitfalls in translating ‘run to completion’ models into Event-B refinements and suggest a solution. We illustrate the approach using our prototype translation tools and show by example, how a synchronisation property between parallel Statecharts can be automatically proven at an intermediate refinement level.