Abstract
This paper presents the Electrum Analyzer, a free-software tool to validate and perform model checking of Electrum specifications. Electrum is an extension of Alloy that enriches its relational logic with LTL operators, thus simplifying the specification of dynamic systems. The Analyzer supports both automatic bounded model checking, with an encoding into SAT, and unbounded model checking, with an encoding into SMV. Instance, or counter-example, traces are presented back to the user in a unified visualizer. Features to speed up model checking are offered, including a decomposed parallel solving strategy and the extraction of symbolic bounds. Source code: https://github.com/haslab/ElectrumVideo: https://youtu.be/FbjlpvjgMDA. © 2018 Copyright held by the owner/author(s).

Abstract
The Robot Operating System (ROS) is an open source framework for the development of robotic software, in which a typical system consists of multiple processes communicating under a publisher-subscriber architecture. A great deal of development time goes into orchestration and making sure that the communication interfaces comply with the expected contracts (e.g. receiving a message leads to the publication of another message). Orchestration mistakes are only detected during runtime, stressing the importance of component and integration testing in the verification process. Property-based Testing is fitting in this context, since it is based on the specification of contracts and treats tested components as black boxes, but there is no support for it in ROS. In this paper, we present a first approach towards automatic generation of test scripts for property-based testing of various configurations of a ROS system.

Abstract
The University of Trás-os-Montes e Alto Douro (UTAD), in an effort to streamline processes and reduce bureaucracy, decided to develop and use an in-house document management system to handle processes. However, this practice created additional needs such as the actual digital signing of documents associated with the institution business and administrative processes. This paper explores a solution proposal to this problem, documenting what are its functionalities and how it works. An initial application of the developed solution is also described and analyzed in order to demonstrate the overall adequacy of the proposed artefact and its overall impact to the institution administrative operations. © Springer International Publishing AG, part of Springer Nature 2018.

Abstract
In this work, we propose a lightweight approach for keyword extraction and ranking based on an unsupervised methodology to select the most important keywords of a single document. To understand the merits of our proposal, we compare it against RAKE, TextRank and SingleRank methods (three well-known unsupervised approaches) and the baseline TF. IDF, over four different collections to illustrate the generality of our approach. The experimental results suggest that extracting keywords from documents using our method results in a superior effectiveness when compared to similar approaches.

Abstract

Abstract
The applications of the blockchain technology are still being discovered. When a new potential disruptive technology emerges, there is a tendency to try to solve every problem with that technology. However, it is still necessary to determine what approach is the best for each type of application. To find how distributed ledgers solve existing problems, this study looks for blockchain frameworks in the academic world. Identifying the existing frameworks can demonstrate where the interest in the technology exists and where it can be missing. This study encountered several blockchain frameworks in development. However, there are few references to operational needs, testing, and deploy of the technology. With the widespread use of the technology, either integrating with pre-existing solutions, replacing legacy systems, or new implementations, the need for testing, deploying, exploration, and maintenance is expected to intensify. © 2020, Springer Nature Switzerland AG.