Transformação de requisitos escritos em português para propriedades lógicas temporais

Abstract

Devido ao aumento na complexidade dos softwares, é fundamental encontrar meios que garantam que os softwares sejam seguros e livres de falhas. A verificação de modelos formais permite que falhas sejam encontradas ainda no início do projeto. A modelagem formal, no entanto, não é tão difundida na indústria quanto a modelagem semi-formal (como a UML). Este trabalho apresenta uma tradução de requisitos escritos em linguagem natural (Português) para propriedades temporais formais. As propriedades foram traduzidas utilizando duas abordagens de processamento de linguagem natural: tradução baseada em regras e tradução baseada em redes neurais. A partir da utilização dessas duas abordagens, as propriedades escritas em linguagem natural foram traduzidas para linguagem de entrada do verificador de modelos UPPAAL. O processamento de linguagem natural foi aplicado nos casos de estudo: Jantar dos Filósofos, Protocolo de Fischer e Base de Dados de Dwyer, para verificar a viabilidade do uso de um tradutor de propriedades. Os resultados obtidos foram satisfatórios.

Abstract: The complexity of software has increased, and therefore it is essential to find ways to ensure that software is safe, and error free. The verification of formal models allows to find inconsistencies at the beginning of the project. Formal modeling, however, is not as used in industry as semi-formal modeling (such as UML). This work presents a translation of natural language writings - Portuguese for formal properties. The properties were formalized using two natural language processing approaches: Rule-based translation and neural network-based translation. From the use of these two approaches, properties written in natural language were translated to the formal input language of the UPPAAL verifier. To verify the possibility of using a property translator, natural language processing was found in the use cases: Philosophers' Dinner, Fischer Protocol and Dwyer Database. The results obtained were satisfactory.