Current Students

André Santos [PhD]

Safety Verification for ROS Applications
Co-supervision with Nuno Macedo.

Chong Liu [PhD]

Lightweight Trustworthy High-Level Software Design
Co-supervision with Nuno Macedo.

Former Students

José Pereira [2016, MSc]

A Web-based Social Environment for Alloy
Co-supervision with Nuno Macedo.

Alloy is a declarative specification language which describes rules and complex structural behaviors. Alloy Analyzer is used to analyze this specifications, this tool generates con- crete instances from the invariants specified in a model, it simulates sequences of defined operations and verifies whether properties introduced are valid or not. Currently, the tool is available as a runnable .jar and it contains a trivial GUI to interact with it. Being such, it requires JAVA installed. It’s in the best interest of the community to achieve and easier access to this tool through a web platform that shall support it in real time and also allow sharing models developed in it by users. Formal methods of software development are growing and they would also benefit from the constructive feedback obtained through this platform regarding the Alloy language/tool.

Eduardo Pessoa [2016, MSc]

Parallel verification of Dynamic Systems with Rich Configurations
Co-supervision with Nuno Macedo.

Model checking is a technique used to automatically verify a model which represents the specification of some system. To ensure the correctness of the system the verification of both static and dynamic properties is often needed.
The specification of a system is made through modeling languages, while the respective verification is made by its model-checker. Most modeling frameworks are not ready to verify models rich in both kind of properties thereby limiting the verification of dynamic systems with rich configurations.
Electrum is a modeling language which mixes the best of the Alloy and TLA specification lan- guages, with the capability of handling the problem mentioned above. This language is supported by two model-checking techniques – one bounded and one unbounded.
Nonetheless, the Electrum’s bounded model-checker has limitations, thus, this dissertation aims to overcome them with the purpose of improving the analysis procedure of Electrum models, in partic- ular, the definition of a new Electrum’s semantics through a translation into Kodkod as well as the creation of a novel procedure of verifying Electrum models in parallel. Hence, in order to achieve these goals, a temporal extension to the Kodkod constraint solver was implemented.

Ana Garis [2015, PhD]

Model-driven Software Development with Alloy
Co-supervision with Daniel Riesco.

Model-Driven Software Development (MDSD) aims at improving the software development process by making extensive use of models at different levels of abstraction. In this model-centric approach, implementations are obtained by step-wise refinements of high-level specifications, ideally deployed as automated models transformations. Following good software engineering principles, quality should be pervasive in all this process, and considerable research effort have been devoted to subjects such as model validation and verification or Model Based Testing (MBT).
Quality assurance in MDSD can be taken to a new level if Formal Methods (FM) are brought into the scene. In fact, besides being both model-centric, both areas share some concerns at their core. Given a formal model that specifies the behavior of a software system, model validation and verification is also a key activity in FM: how to ensure that the model behaves as expected? Another key activity, directly related to model transformation, concerns the formal rela- tion between specifications (abstract models) and implementations: how can we derive a correct implementation from a given specification? Or, alternatively, how to guarantee that a given implementation enjoys the same behavior as the specification?
This project aims at harnessing the FM and software engineering expertise of its research team in the development of high-assurance tools and techniques for MDSD. We intend to address each of the above questions by proposing an Alloy-centric formal approach to MDSD. Alloy [2] is an increasingly popular modeling language developed at the MIT. It shares some resemblances with UML enriched with Object Constraint Language (OCL) constraints, but was designed with automated analysis in mind. Alloy is particularly well-suited to be the ”Trojan horse” of FM in the MDSD community, mainly because it embodies a so-called lightweight approach to formal methods: a language based on the simple mathematical notion of relation, combined with a powerful automatic SAT analyzer, brings the power of formal validation to the average software engineer.
Although Alloy is reaching a mature state as a modeling language, consider- able work is still needed to unleash its full potential for MDSD. This thesis will address precisely one of the most pertinent issues preventing the adoption of Alloy by the overall software engineering community: the lack of a well established and formal methodology to derive high-assurance implementations from Alloy specifications.

Luís Romano [MSc, 2015]

File carving with Haskell
Co-supervision with José Bernardo Barros.

File carving is a technique used to recover erased files from a digital device, when there is no access to their metadata. It is a branch of Digital Forensics, because it is often used to analyse data on a digital device belonging to someone suspect of performing criminal activities.
When one wants to recover data, it’s important to take into account factors as performance, the possibility that a file might be fragmented or that some data is corrupted. While many techniques to recover fragmented files have been proposed, the carvers used in practice almost never recover them, many of them not even trying it.
After a survey on the state of the art of file carving, two main research subjects were chosen. The first one is to understand if multi-core programming can be used to increase performance on current carvers. Most carvers and carving techniques were proposed around 10 years ago, when cheap multi- cores were not widely available. Because of that, carvers don’t make use of all the potential of modern computers, and we will research whether introducing parallelism on a carver can increase its performance. The second topic is understanding why most carvers don’t even attempt to recover fragmented files, when many techniques have been proposed. We will focus on context model carving, which is one of these techniques, and try to understand why this technique was only tried as an academic exercise. General conclusions on recovering fragmented files will also be drawn based on the experiments.

André Santos [MSc, 2015]

Applying Coding Standards to the Robot Operating System
Co-supervision with Nuno Macedo.

Software static analysis is a key component of formal software verification. It consists on inspecting code, using automated tools, to determine a set of relevant properties without executing the program. An example of such properties is the compliance with certain coding standards - sets of rules, subsets of the programming languages, defined to achieve high-quality software, minimizing risks and main- tenance costs. Some coding standards, such as MISRA C++ or HIC++, are highly adopted nowadays, in safety-critical systems with high reliability requirements.
Recent developments in robotics increased human-robot interaction, and show a tendency to intro- duce robots in safety-critical applications, such as transportation and health. As a consequence, it is imperative to guarantee the reliability and quality of the software used to control these robots. This research project shall evaluate the suitability of existing coding standards in the context of the Robot Operating System (ROS), and then develop a generic platform to verify compliance with standards and assure high quality robotics software. Kobuki, a ROS mobile robot, is used as a case study.

Miguel Costa [MSc, 2015]

Software Quality for the Robot Operating System
Co-supervision with Nuno Macedo.

The huge development in the fields of robotics spurred a greater interaction between human beings and robots. It is common knowledge that the malfunctioning of robots may cause not only material damage, but also physical damages to its users. Hence, it is necessary to ensure that robots have proper operation, and one way to ensure this is through the use of high quality software.
In software engineering context there is the ability to assess the quality of the developed soft- ware. This quality will differ depending on whether the code meets all the requirements and specifications proposed by a certain quality model. The code quality can be measured through the study of internal quality components, more particularly the Maintainability.
The methods used for measuring the code quality are complex and can include compliance with standards of different quality models such as ISO 90001.
This research project has as main objective the assessment of the code quality of several robots, developed from ROS. The assessment of this kind of information, about the code quality, is achieved through the use of static analysis tools. These tools, in turn, are responsible for conducting an analysis to source code, measuring its internal quality metrics without having to execute it.

Nuno Macedo [2014, PhD]

A relational approach to bidirectional transformation

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 such area, where such techniques are essential to maintain the consistency between multiple coexisting and simultaneously evolving models.
However, certain characteristics of MDE require a more in-depth analysis in order to be supported by bidirectional model transformations, the lack of which has hindered the development of bidirectional transformation techniques that are effective in 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.

Daniel Murta [2014, MSc]

A comparison between DSLs and GPLs for the implementation of unidirectional and bidirectional transformations

Model-Driven Engineering (MDE) is a software development paradigm based on two building con- cepts: models and transformations. In an early stage, software is abstracted by models, which gradually evolve into the final product by the application of transformations. This dissertation focus essen- tially on transformations. Initially, a general categorisation of transformations is given by presenting the several aspects on which they can be distinguished. One of those aspects is directionality, where transformations are split into one of two categories: unidirectional; or bidirectional.
Then two distinct problems are presented, for which a transformation is proposed as a solution for each. For the first problem, a unidirectional transformation is recommended and for the latter a bidirectional transformation is recommended. For each transformation, two different implementations are conceived and discussed. One of the implementations is achieved by recurring to a Domain- Specific Language (DSL) specifically tailored for the specification of the transformation in case, and the other implementation is materialised by recurring to a General-Purpose Programming Language (GPPL).
The main aim of this thesis is to compare between DSLs and GPPLs as possible alternatives to specify model transformations. This comparison is done by taking into consideration both the unidirectional and bidirectional case scenarios, and by having as comparison guidelines performance and maintainability.

Tiago Jorge [2014, MSc]

A Model Repair Application Scenario with PROVA

Model-Driven Engineering (MDE) is a well known approach to software development that promotes the use of structured specifications, referred to as models, as the primary development artifact. One of the main challenges in MDE is to deal with a wide diversity of evolving models, some of which developed and maintained in parallel. In this setting, a particular point of attention is to manage the model inconsistencies that become inevitable, since it is too easy to make contradictory design decisions and hard to recognise them. In fact, during the development process, user updates will undoubtedly produce inconsistencies which must eventually be repaired. Tool support for this task is then essential in order to automate model repair, so consistency can be easily recovered. However, one of the main challenges in this domain is that for any given set of inconsistencies, there exists an infinite number of possible ways of fixing it. While much of researchers recognise this fact, the way in which this problem should be resolved is far from being agreed upon, and methods on how to detect and fix inconsistencies vary widely. In this master dissertation a comparison between different approaches is done and an application scenario is explored in close collaboration with industry. An off-the-shelf model repair tool leveraging the power of satisfiability (SAT) solving is put to test, while an incremental technique of complex repair trees is implemented and evaluated as a promising, yet very distinctive competitor.

Nuno Rocha Sousa [2014, MSc]

Bidirectinal Distributed Data Aggregation
Co-supervision with Paulo Sérgio Almeida.

Transforming data between two different domains is a typical problem in software engineering. Ideally such transformations should be bidirectional, so that changes in either domain can be propagated to the other one. Many of the existing bidirectional transformation frameworks are instantiations of the so called lenses, proposed as a solution to the well-known view-update problem: if we construct a view that abstracts information in a source domain, how can changes in the view be propagated back to the source? The goal of a distributed data aggregation algorithm is precisely to compute in one or more network nodes a local view of a given global property of interest. As expected, such algorithms react to updates in the distributed input values, but so far no mechanisms were proposed to bidirectionalize them, so that updates in the computed view can be reflected back to the inputs. The goal of this thesis is precisely to research the viability of such bidirectionalizon in a distributed setting.

Hugo Pacheco [2012, PhD]

Bidirectional Data Transformation by Calculation
Co-supervision with José Nuno Oliveira.

Computing is full of situations where transforming a data format into a different one is essential to ”bridge the gap” between technology layers. Naturally, changes in data formats call for corresponding changes in data values. Moreover, to yield true interoperability, bidirectional transforma- tions capable of translating forward and backward between formats are essential. A formal approach to this problem is provided by the 2LT framework (two-level transformation). This framework currently allows the specification of a refinement between an abstract format A and a concrete format B, getting for free the migration functions from values of A to B, and vice-versa.
The main objective of this thesis is to extend the functionality of the 2LT framework in three domains: 1) enlarge the supported set of data formats to cover popular modeling languages; 2) incorporate other kinds of useful bidirectional transformations; 3) allow transformations to be specified using non-deterministic relations instead of functions.

Mário Eiras [2011, MSc]

Formalizing Alloy with a shallow embedding

Formal methods are techniques developed with a mathematical basis in order to ensure a high level of quality on a software product. In this group of techniques there are some which favor the simplicity of use over the reliability of the results in order to reduce the resources that such approaches require. These so called ”lightweight” formal methods emphasize partial specifications and rely on automatic analysis. Alloy is a declarative specification language designed to be ”lightweight”. It was designed along with a model checking tool named Alloy Analyzer which can automatically analyze specifications and search for counter examples in a limited small scope. However, sometimes model checking is not enough and unbounded verification is needed. In this work we defined a strategy to embed the logic of Alloy into the logic of the theorem prover Isabelle/HOL and implemented a tool to automatically perform the embedding, allowing the unbounded verification of Alloy specifications through the use of a theorem prover.

Ricardo Romano [2011, MSc]

Formal approaches to critical systems development: a case study using SPARK

Formal methods comprise a wide set of languages, technologies and tools based on mathematics (logic, set theory) for specification, development and validation of software systems. In some domains, its use is mandatory for certification of critical software components requiring high assurance levels. In this context, the aim of this work is to evaluate, in practice and using SPARK, the usage of formal methods, namely the ”Correctness by Construction” paradigm, in the development of critical systems. SPARK is a subset of Ada language that uses annotations (contracts), in the form of Ada comments, which describe the desired behavior of the component. Our case study is a microkernel of a real-time operating system based on MILS (Multiple Independent Levels of Security/Safety) architecture. It was formally developed in an attempt to cover the security requirements imposed by the highest levels of certification.

Nuno Macedo [2010, MSc]

Translating Alloy Specifications to the Point-free Style

Every program starts from a model, an abstraction, which is iteratively refined until we reach the final result, the implementation. However, at the end, one must ask: does the final program resemble in anyway the original model? Was the original idea correct to begin with? Formal methods guarantee that those questions are answered positively, resorting to mathematical techniques. In particular, in this thesis we are interested on the second factor: verification of formal models. A trend of formal methods defends that they should be lightweight, resulting in a reduced complexity of the specification, and automated analysis. Alloy was proposed as a solution for this problem. In Alloy, the structures are described using a simple mathematical notation: relational logic. A tool for model checking, automatic verification within a given scope, is also provided. However, sometimes model checking is not enough and the need arises to perform unbounded verifications. The only way to do this is to mathematically prove that the specifications are correct. As such, there is the need to find a mathematical logic expressive enough to be able to represent the specifications, while still being sufficiently understandable. We see the point-free style, a style where there are no variables or quantifications, as a kind of Laplace transform, where complex problems are made simple. Being Alloy completely rela- tional, we believe that a point-free relational logic is the natural framework to reason about Alloy specifications. Our goal is to present a translation from Alloy specifications to a point-free relational calculus, which can then be mathematically proven, either resorting to proof assistants or to manual proving. Since our motivation for the use of point-free is simplicity, we will focus on obtaining expressions that are simple enough for manipulation and proofs about them.

João Paz [2010, MSc]

Verifying .QL queries using Alloy

Source code querying tools allow software developers to easily understand and validate their code. SemmleCode is a powerful example of such tools: it is deployed as an Eclipse plug-in for querying Java source code, retrieving metrics, likely bugs and other data. In this thesis we will use Alloy, and its verification tool Alloy Analyzer, to validate source code queries written in .QL, the query language of SemmleCode. For this, we need to dissect SemmleCode and convert its internal data model into a formal Alloy model. The resulting tool allows the programmer to check consistency and equivalence of queries written in .QL, thus helping the programmer to detect irrelevant and ambiguous queries.