A investigação de métodos formais para Engenharia de Requisitos deve considerar alguns aspectos básicos, tais como, modularidade, composição de especificações, diversidade de paradigmas de especificação, domínio de conhecimento.

A complexidade intelectual envolvida no desenvolvimento de sistemas dá origem a duas características aparentemente conflitantes, a saber : modularidade e não monotonicidade. A primeira está relacionada com abordagens que pretendem superar essa complexidade tais como refinamentos sucessivos, que advoga que o produto final seja obtido pela composição de passos mais simples e portanto mais confiáveis. A segunda aparece intrinsecamente relacionada com o processo do desenvolvimento, o qual envolve "bactracking" devido à aprendizagem e revisões. Mais ainda, geralmente sistemas grandes e complexos não apresentam uma homogeneidade suficiente para um único paradigma de especificação.

Tradicionalmente a lógica de primeira ordem tem sido utilizada como formalismo subjacente ao desenvolvimento modular de programas a partir de especificações formais. Mesmo mais recentemente, a lógica de primeira ordem tem sido vastamente empregada como formalismo unificador de especificações escritas segundo diferentes paradigmas.

Por outro a lado a diversidade de domínios de aplicação dos métodos formais tem mostrado a necessidade da utilização de formalismos mais adequados ao tratamento de aspectos para os quais lógica de primeira ordem não se presta, aspectos este tais como incompleteza da informação, manipulação da inconsistência, revisão de conhecimento.

É objetivo desse projeto abordar algumas das questões expostas acima com o propósito de desenvolver um "framework'" formal para Engenharia de Requisitos que incorpore especificações com múltiplos paradigmas, paraconsistência e revisão. Esperamos que nossa abordagem a esses problemas forneça mais um passo na direção da integração do raciocínio não monotônico e desenvolvimento de sistemas.