Ferreira JF, Mendes A, Cunha A, Moreno CB, Silva P, Barbosa LS, Oliveira JN.  2011.  Logic Training through Algorithmic Problem Solving. Tools for Teaching Logic. 6680:62-69. Abstractticttl11.pdf

Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at pre university level, under the justi cation that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The work shop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models.

Cunha A, Oliveira JN, Visser J.  2006.  Type-safe two-level data transformation . FM 2006: Formal Methods. 4085:284-299. Abstract

A two-level data transformation consists of a type-level transformation of a data format coupled with value-level transformations of data instances corresponding to that format. Examples of two-level data transformations include XML schema evolution coupled with document migration, and data mappings used for interoperability and persistence.
We provide a formal treatment of two-level data transformations that is type-safe in the sense that the well-formedness of the value-level transformations with respect to the type-level transformation is guarded by a strong type system. We rely on various techniques for generic functional programming to implement the formalization in Haskell.
The formalization addresses various two-level transformation scenarios, covering fully automated as well as user-driven transformations, and allowing transformations that are information-preserving or not. In each case, two-level transformations are disciplined by one-step transformation rules and type-level transformations induce value-level transformations. We demonstrate an example hierarchical-relational mapping and subsequent migration of relational data induced by hierarchical format evolution.

Santos A, Cunha A, Macedo N, Lourenço CB.  2016.  A Framework for Quality Assessment of ROS Repositories. Abstractros_quality.pdf

Robots are being increasingly used in safety-critical contexts, such as transportation and health. The need for flexible behavior in these contexts, due to human interaction factors or unstructured operating environments, led to a transition from hardware- to software-based safety mechanisms in robotic systems, whose reliability and quality is imperative to guarantee. Source code static analysis is a key component in formal software verification. It consists on inspecting code, often using automated tools, to determine a set of relevant properties that are known to influence the occurrence of defects in the final product. This paper presents HAROS, a generic, plug-in-driven, framework to evaluate code quality, through static analysis, in the context of the Robot Operating System (ROS), one of the most widely used robotic middleware. This tool (equipped with plug-ins for computing metrics and conformance to coding standards) was applied to several publicly available ROS repositories, whose results are also reported in the paper, thus providing a first overview of the internal quality of the software being developed in this community.

Macedo N, Brunel J, Chemouil D, Cunha A, Kuperberg D.  2016.  Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2016). 14.pdf
Macedo N, Cunha A, Guimarães T.  2015.  Exploring Scenario Exploration. Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering. Abstractfase15var.pdf

Model finders are very popular for exploring scenarios, helping users validate specifications by navigating through conforming model instances. To be practical, the semantics of such scenario exploration operations should be formally defined and, ideally, controlled by the users, so that they are able to quickly reach interesting scenarios.
This paper explores the landscape of scenario exploration operations, by formalizing them with a relational model finder. Several scenario exploration operations provided by existing tools are formalized, and new ones are proposed, namely to allow the user to easily explore very similar (or different) scenarios, by attaching preferences to model elements. As a proof-of-concept, such operations were implemented in the popular Alloy Analyzer, further increasing its usefulness for (user-guided) scenario exploration.

Cunha A, Macedo N, Guimarães T.  2014.  Target oriented relational model finding. 7th International Conference on Fundamental Approaches to Software Engineering - FASE. 8411 AbstractPaper

Model finders are becoming useful in many software engineering problems. Kodkod is one of the most popular, due to its support for relational logic (a combination of first order logic with relational algebra operators and transitive closure), allowing a simpler specification of constraints, and support for partial instances, allowing the specification of a priori (exact, but potentially partial) knowledge about a problem's solution. However, in some software engineering problems, such as model repair or bidirectional model transformation, knowledge about the solution is not exact, but instead there is a known target that the solution should approximate. In this paper we extend Kodkod's partial instances to allow the specification of such targets, and show how its model finding procedure can be adapted to support them (using both PMax-SAT solvers or SAT solvers with cardinality constraints). Two case studies are also presented, including a careful performance evaluation to assess the effectiveness of the proposed extension.

Macedo N, Cunha A, Pacheco H.  2014.  Towards a framework for multi-directional model transformations. 3rd International Workshop on Bidirectional Transformations - BX. 1133 AbstractPaper

The Query/View/Transformation Relations (QVT-R) standard for bidirectional model transformation is notorious for its underspecified semantics. When restricted to transformations between pairs of models, most of the ambiguities and omissions have been addressed in recent work. Nevertheless, the application of the QVT-R language is not restricted to that scenario, and similar issues remain unexplored for the multidirectional case (maintaining consistency between more than two models), that has been overlooked so far.
In this paper we first discuss ambiguities and omissions in the QVT-R standard concerning the mutidirectional transformation scenario, and then propose a simple extension and formalization of the checking and enforcement semantics that clarifies some of them. We also discuss how such proposal could be implemented in our Echo bidirectional model transformation tool.
Ours is just a small step towards making QVT-R a viable language for bidirectional transformation in realistic applications, and a considerable amount of basic research is still needed to fully accomplish that goal.

Macedo N, Pacheco H, Sousa NR, Cunha A.  2014.  Bidirectional Spreadsheet Formulas. VL/HCC - IEEE Symposium on Visual Languages and Human-Centric Computing. 6120 Abstractvlhcc14ss.pdf

Bidirectional transformations have potential applications in a vast number of computer science domains. Spreadsheets, on the other hand, are widely used for developing business applications, but their formulas are unidirectional, in the sense that their result can not be edited and propagated back to their input cells. In this paper, we interpret such formulas as a well-known class of bidirectional transformations that go by the name of lenses. Being aimed at users that are not proficient with programming languages, we devote particular attention to the seamless embedding of the proposed bidirectional mechanism with the typical workflow of spreadsheet environments, allowing users to have a fine control and understanding of the behavior of the derived backward transformations.

Cunha A.  2014.  Bounded Model Checking of Temporal Formulas with Alloy. Lecture Note in Computer Science. 8477 Abstract1207.2746v2.pdf

Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be performed with the Alloy Analyzer.

Cunha A, Anjorin A, Giese H, Hermann F, Rensink A, Schurrr A.  2014.  BenchmarX. EDBT/ ICDT Workshops. 1133 Abstractpaper-13.pdf

Bidirectional transformation (BX) is a very active area of research interest. There is not only a growing body of theory, but also a rich set of tools supporting BX. The problem now arises that there is no commonly agreed-upon suite of tests or benchmarks that shows either the conformance of tools to theory, or the performance of tools in particular BX scenarios. This paper sets out to improve the state of affairs in this respect, by proposing a template and a set of required criteria for benchmark descriptions, as well as guidelines for the artifacts that should be provided for each included test. As a proof of concept, the paper additionally provides a detailed description of one concrete benchmark.

Cunha A, Macedo N, Guimarães T.  2013.  Model Repair and Transformation with Echo. 28th International Conference on Automated Software Engineering - ASE. 6138:694–697. Abstractase13.pdf

Models are paramount in model-driven engineering. In a software project many models may coexist, capturing different views of the system or different levels of abstraction. A key and arduous task in this development method is to keep all such models consistent, both with their meta-models (and the respective constraints) and among themselves. This paper describes Echo, a tool that aims at simplifying this task by automating inconsistency detection and repair using a solver based engine. Consistency between different models can be specified by bidirectional model transformations, and is guaranteed to be recovered by minimal updates on the inconsistent models. The tool is freely available as an Eclipse plugin, developed on top of the popular EMF framework, and supports constraints and transformations specified in the OMG standard languages OCL and QVT-R, respectively.

Cunha A, Macedo N.  2013.  Implementing QVT-R Bidirectional Model Transformations Using Alloy. 16th International Conference on Fundamental Approaches to Software Engineering - FASE. 7793:297–311. Abstractfase13.pdf

QVT Relations (QVT-R) is the standard language proposed by the OMG to specify bidirectional model transformations. Unfortunately, in part due to ambiguities and omissions in the original seman- tics, acceptance and development of effective tool support has been slow. Recently, the checking semantics of QVT-R has been clarified and formalized. In this paper we propose a QVT-R tool that complies to such semantics. Unlike any other existing tool, it also supports meta-models enriched with OCL constraints (thus avoiding returning ill-formed models), and proposes an alternative enforcement semantics that works ac- cording to the simple and predictable “principle of least change”. The implementation is based on an embedding of both QVT-R transformations and UML class diagrams (annotated with OCL) in Alloy, a lightweight formal specification language with support for automatic model finding via SAT solving.

Cunha A, Oliveira JN, Macedo N, Pacheco H.  2013.  Composing least-change lenses. Proceedings of the First International Workshop on Bidirectional Transformations (BX 2012). 57:19. Abstractbx13.pdf

Non-trivial bidirectional transformations (BXs) are inherently ambiguous, as there are in general many different ways to consistently translate an update from one side to the other. Existing BX languages and frameworks typically satisfy fundamental first principles which ensure acceptable and stable (well-behaved) translation. Unfortunately, these give little insight about how a particular update translation is chosen among the myriad possible. From the user perspective, such unpredictability may hinder the adoption of BX frameworks.
The problem can be remedied by imposing a “principle of least change” which, in a state-based framework, amounts to translating each update in a way such that its result is as close as possible to the original state, according to some distance measure.
Starting by formalizing such BXs focusing on the particular framework of lenses, this paper discusses whether such least-change lenses can be defined by composition, an essential construct of BX frameworks. For sequential composition, two (dual) update translation alternatives are presented: a classical deterministic one and a nondeterministic. A key ingredient of the approach is the elegant formalization of the main concepts in relation algebra, which exposes several similarities and dualities.

Macedo N, Pacheco H, Cunha A.  2012.  Relations as executable specifications: taming partiality and non-determinism using invariants. 13th International Conference on Relational and Algebraic Methods in Computer Science - RAMICS. LNCS 7560:146–161. Abstractndlenses12.pdf

The calculus of relations has been widely used in program specification and reasoning. It is very tempting to use such specifications as running prototypes of the desired program, but, even considering finite domains, the inherent partiality and non-determinism of relations makes this impractical and highly inefficient. To tame partiality we prescribe the usage of invariants, represented by coreflexives, to characterize the exact domains and codomains of relational specifications. Such invariants can be used as pre-condition checkers to avoid runtime errors. Moreover, we show how such invariants can be used to narrow the non-deterministic execution of relational specifications, making it viable for a relevant class of problems. In particular, we show how the proposed techniques can be applied to execute specifications of bidirectional transformations, a domain where partiality and non-determinism are paramount.

Cunha A, Pacheco H.  2012.  Multifocal: A Strategic Bidirectional Transformation Language for XML Schemas. Proceedings of the 5th International Conference on Model Transformation - ICMT. 7307:89–104. Abstracticmt12.pdf

Lenses are one of the most popular approaches to define bidirectional transformations between data models. However, writing a lens transformation typically implies describing the concrete steps that convert values in a source schema to values in a target schema. In contrast, many XML-based languages allow writing structure-shy programs that manipulate only specific parts of XML documents without having to specify the behavior for the remaining structure. In this paper, we propose a structure-shy bidirectional two-level transformation language for XML Schemas, that describes generic type-level transformations over schema representations coupled with value-level bidirectional lenses for document migration. When applying these two-level programs to particular schemas, we employ an existing algebraic rewrite system to optimize the automatically-generated lens transformations, and compile them into Haskell bidirectional executables. We discuss particular examples involving the generic evolution of recursive XML Schemas, and compare their performance gains over non-optimized definitions.