Refinement and Verification of Responsive Control Systems

Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods. Open image in new window , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage Open image in new window tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Open image in new window refinements and suggest a solution. We outline how safety and liveness properties could be verified.