Proposta de táticas para prova de teoremas de gramática de grafos.

Abstract

Computation is used daily in the modern world through systems that are becoming more complex each day. The occurrence of errors in these programs execution is increasing and causing many kinds of losses to the people. So, it is a need to use some ways to increase the reliability of those systems. One way to develop more reliable systems is by the use of formal methods. Inside these techniques there are the formal specification and verification. An attractive language for formal specification is the graph grammars (GG), since it is visual and based in a simple mechanism of rewriting rules. In the other side, the verification can be done by the technique of theorem proving, that allows the proof of properties for systems with wide space of states, or even infinite states. There is an approach that allows the use of the theorem proving technique for systems described by GG. In this proposal, GG was translated to Event-B language, which makes possible the utilization of Rodin platform to the proof of properties. At the verification step some statement obligations are generated and which must be demonstrated. Some of them are unloaded automatically and some others need a experienced user intervention. This intervention, in most of cases, is not trivial and restricts the usage of the technique. This work aims to optimize the verification process, proposing some proof tactics in order to demonstrate interactive obligations, which angle to help the developer in the moment of verification. Firstly, strategies to a GG system proof obligations patterns are presented. Just after, tactics to demonstrate specific properties obligations are suggested. The presentation of the tactics is done by describing the main steps to the demonstrations of the considered properties, describing the proof tree and proposing usage trees. For any of those forms it is possible to present the corresponding proof of the obligation.