Abstract

Abstract
Formal verification has become increasingly crucial in ensuring the accurate and secure functioning of modern software systems. Given a specification of the desired behaviour, i.e. a contract, a program is considered to be correct when all possible executions guarantee the specification. Should the software fail to behave as expected, then a bug is present. Most existing research assumes that the bug is present in the implementation, but it is also often the case that the specified expectations are incorrect, meaning that it is the specification that must be repaired. Research and tools for providing alternative specifications that fix details missing during contract definition, considering that the implementation is correct, are scarce. This paper presents a preliminary tool, focused on Dafny programs, for automatic specification repair in contract programming. Given a Dafny program that fails to verify, the tool suggests corrections that repair the specification. Our approach is inspired by a technique previously proposed for another contract programming language and relies on Daikon for dynamic invariant inference. Although the tool is focused on Dafny, it makes use of specification repair techniques that are generally applicable to programming languages that support contracts. Such a tool can be valuable in various scenarios, such as when programmers have a reference implementation and need to analyse their contract options, or in educational contexts, where it can provide students with hints to correct their contracts. The results of the evaluation show that the approach is feasible in Dafny and that the overall process has reasonable performance but that there are stages of the process that need further improvements.

Abstract
The ubiquity of data transformation problems in software engineering has led to the development of bidirectional transformation techniques in a variety of application domains. Model-driven engineering (MDE) is one of those areas, where such techniques are essential to maintain the consistency between multiple coexisting and simultaneously evolving models. However, the lack of in-depth research about certain characteristics of MDE has hindered the development of effective bidirectional model transformations that are able to address realistic MDE scenarios. This dissertation tackles two of these issues: that of constrained transformation domains and least-change transformations. The first regards the transformations’ ability to take into consideration the constraints imposed by the meta-models, and is essential to achieve correctness; the second regards the transformations’ ability to control the selection of updates from among those considered correct, and is essential to achieve a predictable system. These two issues are addressed under two popular bidirectional transformation schemes: in the context of the asymmetric framework of lenses, following a combinatorial approach; and in the context of the symmetric framework of constraint maintainers, proposing a solution based on model finding. The latter was effectively deployed as Echo, a tool for model repair and transformation. The expressiveness and flexibility provided by relational logic enabled it to be used as the unifying formalism throughout this dissertation.;A ubiquidade de problemas de transformação de dados em engenharia de software levou ao desenvolvimento de técnicas para transformação bidirecional numa variedade de domínios de aplicação. A Engenharia Baseada em Modelos (MDE) é uma dessas áreas, onde essas técnicas são essenciais para gerir a consistência entre múltiplos modelos que coexistem e evolvem simultaneamente. No entanto, a falta de estudos aprofundados sobre algumas características da MDE tem dificultado o desenvolvimento de técnicas de transformação bidirecional de modelos eficazes e que consigam lidar com cenários MDE realísticos. Esta dissertação aborda dois destes problemas: o de domínios de transformação restringidos e o de transformações com mudanças-mínimas. O primeiro tem que ver com a capacidade das transformações de ter em consideração as restrições impostas pelos meta-modelos e é essencial para atingir correcção; a segunda tem que ver com a capacidade de controlar a seleção de modificações entre as consideradas corretas, e é essencial para obter um sistema previsível. Esta tese aborda estes dois problemas sob dois populares esquemas de transformação bidirecional: no contexto da framework assimétrica das lentes, seguindo uma abordagem combinatorial, e no contexto da framework simétrica dos constraint maintainers, sendo proposta uma solução baseada em “procura de modelos”. Esta última foi efetivamente implementada como Echo, uma ferramenta para a reparação e transformação de modelos. A expressividade e flexibilidade proporcionada pela lógica relacional permitiu que esta fosse usada como o formalismo unificador desta dissertação.

Abstract
Background: Many progranunmg environments include automated feedback in the form of hints to help novices learn autonomously. Some experimental studies investigated the impact of automated liints in the immediate, performance and learning retention in that context. Automated feedback is also becoming a popular research topic in the context of formal specification languages, but so far no experimental studies have been conducted to assess its impact while learning such languages. Objective: We aim to investigate the impact of different types of automated hints while learning a formal specification language, not only in terms of immediate performance and learning retention, but also in the emotional response of the students. Method: We conducted a simple one-factor randomised experiment in 2 sessions involving 85 BSc students majoring in CSE. In the 1st session students were divided in 1 control group and 3 experimental groups, each receiving a different type of hint while learning to specify simple, requirements with the Alloy formal specification language. To assess the impact of hints on learning retention, in the 2nd session, 1 week later, students had no hints while formalising requirements. Before and after each session the students answered a standard self-reporting emotional survey to assess their emotional response to the experiment. Results: Of the 3 types of hints considered, only those pointing to the precise location of an error had a positive impact on the immediate performance and none had significant impact in learning retention. Hint availability also causes a significant impact on the emotional response, but no significant emotional :impact exists once hints are no longer available (i.e. no deprivation effects were detected). Conclusion: Although none of the evaluated hints had an impact on learning retention, learning a formal specification language with an environment that provides hints with precise error locations seems to contribute to a better overall experience without apparent drawbacks. Further studies are needed to investigate if other kind of feedback, namely hints combined with some sort of self explanation prompts, can have a positive impact in learning retention.

Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

Abstract
Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.