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