Propostas para Dissertação

Mestrados no Departamento de Informática

Consultar ficha completa de uma proposta de dissertação

proponente: Alcino Cunha e Nuno Macedo
instituição/empresa: Universidade do Minho
tema/título: Studying the Impact of Scenario Exploration in Software Design
área científica: Software Engineering
local: Braga
curso de mestrado: Mestrado Integrado em Engenharia Informática
Trustworthy software design is essential to achieve high-assurance software systems. This process
requires a formal specification language supported by rigorous verification and validation
techniques. Alloy ( is one such framework, providing a simple language
supported by an Analyzer that is able to automatically verify Alloy specifications. This Analyzer
allows users to inspect alternative instances that satisfy desirable properties, easing the
validation process. Although, by default, this scenario exploration procedure generates arbitrary
valid solutions, recent work has proposed alternative and more advanced navigation criteria. Recently, this team has developed a web-browser version of the Alloy Analyzer
( Besides the standard functionalities, this version allows users to
easily share their models and solutions through persistent identifiers, without the need for any
local installation. Moreover, it supports the creation of challenges, incomplete Alloy
specifications which the users are expected to correctly complete. This framework provides an
unique opportunity to register and study the habits of Alloy users, and the steps commonly taken to
achieve correct specifications. The goal of this thesis is to extend Alloy4Fun with functionalities for advanced scenario
exploration, and study its impact on the development of correct Alloy specifications. In
particular, we expect to identify which scenario exploration criteria are more helpful when
validating a model, allowing the users to reach a correct solution quicker.