@inproceedings{b16c8fdff2224c0791cfb883edcb1f06,
title = "Proving Local Invariants in ASTDs",
abstract = "This paper proposes a formal approach for generating proof obligations to verify local invariants in an Algebraic State Transition Diagram (ASTD). ASTD is a graphical specification language that allows for the combination of extended hierarchical state machines using CSP-like process algebra operators. Invariants can be declared at any level in a specification (state, ASTD), fostering the decomposition of system invariants into modular local invariants which are easier to prove, because proof obligations are smaller. The proof obligations take advantage of the structure of an ASTD to use local invariants as hypotheses. ASTD operators covered are automaton, sequence, closure and guard. Proof obligations are discharged using Rodin. When proof obligations cannot be proved, ProB can be used to identify counter-examples to help in correcting/reinforcing the invariant or the specification.",
keywords = "ASTD, ProB, Rodin, invariant, proof obligation",
author = "Quelen Cartellier and Marc Frappier and Amel Mammar",
note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.; 24th International Conference on Formal Engineering Methods, ICFEM 2023 ; Conference date: 21-11-2023 Through 24-11-2023",
year = "2023",
month = jan,
day = "1",
doi = "10.1007/978-981-99-7584-6\_14",
language = "English",
isbn = "9789819975839",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "228--246",
editor = "Yi Li and Sofi{\`e}ne Tahar",
booktitle = "Formal Methods and Software Engineering - 24th International Conference on Formal Engineering Methods, ICFEM 2023, Proceedings",
}