@inproceedings{f0bc6b834de94467b31a7705b15089b2,
title = "A Rodin Plugin for Generating Proof Obligations for Invariant Preservation for ASTDs",
abstract = "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.",
keywords = "ASTD, Invariant, Proof obligation, Rodin",
author = "Quelen Cartellier and Marc Frappier and Amel Mammar",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.; 23rd International Conference on Software Engineering and Formal Methods, SEFM 2025 ; Conference date: 10-11-2025 Through 14-11-2025",
year = "2026",
month = jan,
day = "1",
doi = "10.1007/978-3-032-10444-1\_10",
language = "English",
isbn = "9783032104434",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "157--164",
editor = "Domenico Bianculli and Elena Gomez-Martinez",
booktitle = "Software Engineering and Formal Methods - 23rd International Conference, SEFM 2025, Proceedings",
}