Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)

AUTOR(ES)
DATA DE PUBLICAÇÃO

2005

RESUMO

This work presents a technique of formal verication of Procedural Reasoning System - PRS, a programming language that uses the procedural reasoning approach. This technique is based on the use of conversion rules between PRS programs and Coloured Petri Nets (CPNs). To this end, conversion rules of a subgroup of the majority of the syntax used in language PRS for RPC are presented. In order to proceed to formal verication of program specied in PRS we use the CPNs formalism (verication of the structural and dynamic properties) to formaly analyze the equivalent PRS programs. We use available computational tools to draw, to simulate and to analyze the generated Coloured Petri Nets. If we have the conversion rules PRS-CPN, we can do this conversion in a strict manual way. However, the probability of introduction of errors in the conversion is great, and the effort necessary to guarantee the correctness of the manual conversion is of the same order of magnitude that the elimination of eventual errors directly in the original PRS program. Thus, the automatized conversion is of great importance to prevent that the manual conversion leads to undesirable errors, which can invalidate all the conversion process. The main contribution of this research work consist in the development of an autmomatized formal verication techique consisting of of two distinct stages, even so interrelated. The rst stage is the presentation of conversion rules between PRS-CPN. The second phase is related to the development of a converter to automatically transform the programs PRS for CPN. Automatic conversion is possible, because all the presented rules of conversion follow generic formation laws, which can be enclosed in algorithms

ASSUNTO(S)

redes de petri coloridas procedural reasoning system sistema de raciocínio procedural verificação formal coloured petri nets engenharia eletrica formal verification

ACESSO AO ARTIGO

Documentos Relacionados