Title :
Towards the Use and Description of Proof Tactics for Theorem Proving Graph Grammars through Rodin
Author :
Lemos, Luiz Carlos ; Da Costa Cavalheiro, Simone Andre ; Foss, Luciana
Author_Institution :
Technol. Dev. Center, Fed. Univ. of Pelotas, Pelotas, Brazil
Abstract :
Graph grammar is a formal language suitable for the specification of distributed and concurrent systems. Theorem proving is a technique that allows the verification of systems with huge (and infinite) state space. A previous approach has proposed proof strategies to help the developer in the verification process through theorem proving, when adopting graph grammar as specification language. This paper proposes a visual representation for the proposed tactics, in order to turn them even more intuitive and user friendly.
Keywords :
formal languages; graph grammars; specification languages; state-space methods; theorem proving; Rodin; concurrent systems; distributed systems; formal language; proof strategies; proof tactics description; specification language; system verification process; theorem proving graph grammars; visual representation; Antennas; Context; Discharges (electric); Grammar; Mobile communication; Proposals; Visualization; formal methods; graph grammar; theorem proving;
Conference_Titel :
Theoretical Computer Science (WEIT), 2013 2nd Workshop-School on
Conference_Location :
Rio Grande
DOI :
10.1109/WEIT.2013.24
