Current Students
Hugo Pacheco [PhD]
Bidirectional Data Transformation by CalculationCo-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.
Ana Garis [PhD]
Model-driven Software Development with AlloyCo-supervision with Daniel Riesco.
Nuno Macedo [PhD]
A relational approach to bidirectional transformations
Transforming data between different structures is a typical computing problem. Also, in most cases we wish these transformations to be bidirectional, with the changes made in either structure reflected in the other. A naive approach to solve this problem involves the creation of two unidirectional transformations and then verify that they are in some way each-other inverses (or well-behaved). Besides being an expensive and error-prone task, this verification would need to be performed everytime the transformation is modified. A better approach consists in designing a language where an expression represents both transformations, which are guaranteed to be correct by construction. A particularly successful mechanism created under these approach are the lenses, proposed as a solution to the view-update problem of databases (how to propagate updates on a database view to the source).
Recent work has been developed to specify these lenses using functional point-free (PF) notation, lifting standard PF combinators and recursion pat- terns to well-behaved lenses. This approach enables easy equational calculation with lenses and optimization of bidirectional transformations. However it has some limitations, namely it is not expressive enough to capture all sorts of bidirectional transformations. In fact, the transformations can be seen as abstraction and representation relations. By generalizing to a relational setting we obtain a higher degree of freedom in the calculus, becoming easier to calculate inverses of transformations and represent data invariants. Since a PF version of relational calculus has already been widely studied, we believe we can improve this previous work under this perspective.
In particular, the objectives of this thesis are: 1) To compare and classify the existing approaches to bidirectional transfor- mations using the relational calculus as unifying formalism; 2) To propose a methodology for the derivation of inverses by calculation, starting from the specification of the forward transformation and the desired well-behavedness criterion; 3) To enlarge the applicability of the previously proposed PF lens notation, by proposing new combinators and using data invariants to enlarge the expressiveness of the language. 4) To propose an effective technique for bidirectional transformation of non tree-like data structures (graphs and models in general). Some techniques have already been proposed, but they are either too ad-hoc, giving little or no guarantees to the user, or too complex and limited, making it difficult to express transformations or perform calculations / optimizations. 4) To identify and give proper semantics to well-behaved subsets of existing high-level model transformation languages (namely QVT) using the calculus of relations.
Hélder Pereira [MSc]
Model Transformation Between Alloy and VDMCo-supervision with Peter Gorm Larsen.
Alloy and VDM are two popular and well known formal methods built around a state-based modelling language. Both advocate a lightweight approach to formal methods, with emphasis on partial specifications and partial correctness, and a strong tool support. Alloy’s highly declarative modelling language is based on a single principle: everything is a relation. Due to its simplicity and clean semantics in terms of first order logic, its specifications can be model-checked in the Alloy Analyzer using off-the-shelf SAT solvers, providing immediate feedback to the designer. On the other hand, VDM’s modelling language is more similar to standard functional programing languages, with a useful range of composite types that simplify the modelling task. It also allows one to write executable specifications, that can be later used by VDM Tools for test based analysis. VDM Tools also allow automatic code generation to C++ and Java, and automatic proof obligation generation to HOL. VDM also has extensions to model object orientation, concurrency and real-time systems.
Given that each of these formal methods has its own specific advantages, it would be convenient to use both in the process of rigorous soft- ware development. However, without proper tool support, this would lead to a tedious and error-prone manual translation of specifications written in Alloy to VDM, and vice-versa. The objective of this thesis is precisely to identify a set of rules that can be used for automatic translation between subsets of either language. Following on the tradition of lightweight formal methods, the emphasis shall not be on completeness, but rather on effectiveness: we will focus only on the most common idioms of each language, and the identified rules will be harnessed into a tool for automatic model transformation between Alloy and VDM.
Nuno Correia [MSc]
Conversion of Alloy specifications to JML-annotated Java classesFormer Students
Mário Eiras [2011, MSc]
Formalizing Alloy with a shallow embeddingFormal 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 SPARKFormal 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 StyleEvery 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 AlloySource 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.