Mining hints for fixing formal specifications

Abstract

O crescimento da complexidade de aplicações informáticas tornou falhas e erros de software uma inevitabilidade. Para ajudar a garantir que uma aplicação funciona como previsto, profissionais recorrem a modelos de software para detetar e corrigir problemas nas fases iniciais de desenvolvimento. Especificações formais são modelos de software que permitem a desenvolvedores especificar rigorosamente estruturas e comportamentos de software. Infelizmente, a sua complexidade inerente também pode impor problemas nos principiantes que as tentam aprender. Uma maneira possível de abordar este problema seria o emprego de práticas de reparação de especificações e geração automática de sugestões para ajudar os alunos a corrigir tentativas erradas. Alloy4Fun é uma plataforma online para a aprendizagem de Alloy, uma linguagem de especificação formal com capacidades de analise automática. Alloy4Fun permite a instrutores criar e partilhar desafios de especificação formal com avaliação automática. Recentemente, uma técnica de geração automática de sugestões for desenvolvida para esta plataforma, mas provou ser insatisfatória devido ao seu fraco desempenho. O objetivo desta tese foi explorar outras técnicas para geração de sugestões, nomeadamente técnicas de geração de sugestões baseadas em dados, que poderiam usar o conjunto de dados publico de submissões históricas de estudantes do Aloy4Fun para fornecer dicas de forma mais eficiente. O principal resultado desta tese, SpecAssistant, é um novo sistema de geração de dicas baseado em dados para Alloy. Este extrai informação do conjunto de dados do Alloy4Fun para construir grafos de submissões, dos quais são extraídas sugestões a partir de regras personalizadas pelos desenvolvedores de cada desafio. Para avaliar o SpecAssistant, realizamos uma série de experiências quantitativas, com o objetivo de avaliar a disponibilidade e o desempenho do nosso sistema. As nossas descobertas demostram que o SpecAssistant consegue fornecer dicas para uma porção significativa de submissões, apresentado um desempenho que supera o sistema de sugestões precedente.

The increasing complexity of software applications has made software bugs and errors an inevitability. To help ensure that software functions as intended, professionals rely on software models to detect and correct faults early in the development process. Formal specifications are software models that allow developers to precisely specify software structures and behaviors. Unfortunately, their inherent complexity can also pose problems to newcomers while learning them. One possible way to address this issue could be to employ automated hint and specification repair techniques to help students fix incorrect attempts. Alloy4Fun is an online platform for learning Alloy, a formal specification language with automated analysis features. Alloy4Fun allows educators to create and share specification challenges with automated assessment. Recently, a hint generation technique based on automated repair has been developed for this platform, but proved unsatisfactory due to its poor performance. The goal of this thesis was to explore other techniques for hint generation, namely data-driven hint generation techniques which could leverage the Alloy4Fun public data-set of past student submissions to provide hints more efficiently. The main outcome of this thesis, SpecAssistant, is a new data-driven hint generation system for Alloy. It mines the Alloy4Fun data-set to build submission graphs, from which hints are extracted using policy rules customized by the challenge developers. To evaluate SpecAssistant we performed a series of quantitative experiments, with the goal of assessing our system’s availability and performance. Our findings show that SpecAssistant can provide hints for a significant portion of invalid submissions with a performance that greatly surpasses that of the previous hint system.