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. [inline-graphic not available: see fulltext] , 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 [inline-graphic not available: see fulltext] tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into [inline-graphic not available: see fulltext] refinements and suggest a solution. We outline how safety and liveness properties could be verified.