Towards a quantitative alloy

Abstract

When one comes across a new problem that needs to be solved, by abstracting from its associated details in a simple and concise way through the use of formal methods, one is able to better understand the matter at hand. Alloy (Jackson, 2012), a declarative specification language based on relational logic, is an example of an effective modelling tool, allowing high-level specification of potentially very complex systems. However, along with the irrelevant information, measurable data of the system is often lost in the abstraction as well, making it not as adequate for certain situations. The Alloy Analyzer represents the relations under analysis by Boolean matrices. By extending this type of structure to: • numeric matrices, over N0 , one is able to work with multirelations, i.e. relations whose arcs are weighted; each tuple is thus associated with a natural number, which allows reasoning in a similar fashion as in optimization problems and integer programming techniques; • left-Stochastic matrices, one is able to model faulty behaviour and other forms of quantitative information about software systems in a probabilistic way; in particular, this introduces the notion of a probabilistic contract in software design. Such an increase in Alloy’s capabilities strengthens its position in the area of formal methods for software design, in particular towards becoming a quantitative formal method. This dissertation explores the motivation and importance behind quantitative analysis by studying and establishing theoretical foundations through categorial approaches to accomplish such reasoning in Alloy. This starts by reviewing the required tools to support such groundwork and proceeds to the design and implementation of such a quantitative Alloy extension. This project aims to promote the evolution of quantitative formal methods by successfully achieving quantitative abstractions in Alloy, extending its support to these concepts and implementing them in the Alloy Analyzer.

Quando se depara com um novo problema que precisa de ser resolvido, ao abstrair dos seus detalhes associados de forma simples e concisa recorrendo a métodos formais, é possível compreender melhor o assunto em questão. Alloy (Jackson, 2012), uma linguagem de especificação declarativa baseada em lógica relacional, é um exemplo de uma ferramenta de modelação eficaz, possibilitando especificações de alto-nível de sistemas potencialmente bastante complexos. Contudo, em conjunto com a informação irrelevante, os dados mensuráveis são muitas vezes também perdidos na abstração, tornando-a não tão adequada para certas situações. O Alloy Analyzer representa as relações sujeitas a análise através de matrizes Booleanas. Ao estender este tipo de estrutura para: • matrizes numéricas, em N0 , é possível lidar com multirelações, i.e., relações cujos arcos são pesados; cada tuplo é consequentemente associado a um número natural, o que proporciona uma linha de raciocínio semelhante à de técnicas de problemas de otimização e de programação inteira; • matrizes estocásticas, permitindo a modelação de comportamento defeituoso e de outros tipos de informação quantitativa de sistemas de software probabilisticamente; em particular, é introduzida a noção de contrato probabilístico em design de software. Tal aumento às capacidades do Alloy, fortalece a sua posição na área de métodos formais para design de software, em particular, a caminho de se tornar um método formal quantitativo. Esta dissertação explora a motivação e a importância subjacente à análise quantitativa, a partir do estudo e consolidação dos fundamentos teóricos através de abordagens categóricas de forma a conseguir suportar esse tipo de raciocínio em Alloy. Inicialmente, as ferramentas imprescindíveis para assegurar tal base são analisadas, passando de seguida ao planeamento e posterior implementação de tal extensão quantitativa do Alloy. Este projecto pretende promover a evolução dos métodos formais quantitativos através da concretização de abstracção quantitativa em Alloy, estendendo a sua base para suportar estes conceitos e assim implementá los no Alloy Analyzer.