Esta dissertação apresenta o Specifier, uma framework para engenharia reversa de implementeções black-box usando a linguagem de modelação Alloy. Para usar a framework, um modelo Alloy que representa a estrutura base do sistema ao qual será aplicada engenharia reversa tem de ser desenvolvido. As instâncias deste modelo são depois transformadas em casos de teste para o sistema e o output é usado para determinar se a especificação formal está correta ou não. O objetivo é atingir uma especificação que descreve com exatidão o sistema, completando com sucesso o processo de engenharia reversa. O Specifier foi usado para fazer engenharia reversa da especificação de dois aspetos ambíguos do Alloy Analyzer, nomeadamente o que é considerado um comando válido em Alloy no que toca à definição de escopos e como é que o Alloy Analyzer refina os escopos definidos pelo utilizador.

This dissertation presents Specifier, a framework for reverse engineering black-box implementations using the Alloy formal modelling language. To use the framework, an Alloy model representing the base structure of the system to be reverse engineered has to be developed. The instances from this model are then transformed into test cases for the system and the output is used to determine if the the formal specification is correct or not. The goal is to reach a specification that accurately describes the system, thus successfully completing the reverse engineering process. The Specifier was used to reverse engineer the specification of two ambiguous aspects of Alloy Analyzer, namely what is considered a valid Alloy command in terms of the defined scopes and how the Alloy Analyzer refines the scopes defined by the user.