Santos A, Cunha A, Macedo N.  2019.  Static-time Extraction and Analysis of the ROS. Abstractros_model.pdf

The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system’s architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation
Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before.

Halder R, Proença J, Macedo N, Santos A.  2017.  Formal Verification of ROS-based Robotic Applications using Timed-Automata. FME Workshop on Formal Methods In Software Engineering. ros-formalise17.pdf
Santos A, Cunha A, Macedo N, Arrais R, dos Santos FN.  2017.  Mining the Usage Patterns of ROS Primitives. Abstractros_patterns.pdf

The Robot Operating System (ROS) is nowadays one of the most popular frameworks for developing robotic
applications. To ensure the (much needed) dependability and safety of such applications we forecast an increasing demand for ROS-specific coding standards, static analyzers, and tools alike. Unfortunately, the development of such standards and tools can be hampered by ROS modularity and configurability, namely the substantial number of primitives (and respective variants) that must, in principle, be considered.
To quantify the severity of this problem, we have mined a large number of existing
ROS packages to understand how its primitives are used in practice, and to determine which combinations of primitives are most popular. This paper presents and discusses the results of this study, and hopefully provides some guidance for future standardization efforts and tool developers.

Carvalho M, Belo O, Macedo N.  2017.  Checking the Correctness of What-If Scenarios. 11th IFIP WG 8.9 Working Conference (CONFENIS 2017).
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.

Oliveira B, Belo O, Macedo N.  2016.  Towards a Formal Validation of ETL Patterns Behavior. 6th International Conference on Model and Data Engineering (MEDI 2016).
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, 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.