This paper presents a Rodin plugin for automatically generating proof obligations for invariant preservation to ensure the correctness of an Algebraic State Transition Diagram (ASTD). ASTD is a graphical specification language that allows for the combination of Statechart-like extended hierarchical state machines using CSP-like process algebra operators. Invariants can be attached to any level in an ASTD to specify local properties. This plugin takes as input an ASTD in JSON format and produces the proof obligations within an Event-B context. It implements a formal approach that recursively generates all the proof obligations according to the structure of an ASTD. The tool currently supports automaton, sequence, guard and closure ASTDs, but can be easily extended to consider any ASTD type.