Abstract
This paper presents Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances (including dynamic ones developed with the Electrum extension), to be used mainly in an educational context. By introducing secret paragraphs and commands in the models, Alloy4Fun allows the distribution and automated assessment of simple specification challenges, a mechanism that enables students to learn the language at their own pace. Alloy4Fun stores all versions of shared and analyzed models, as well as derivation trees that depict how they evolved over time: this wealth of information can be mined by researchers or tutors to identify, for example, learning breakdowns in the class or typical mistakes made by Alloy users. Alloy4Fun has been used in formal methods graduate courses for two years and for the latest edition we present results regarding its adoption by the students, as well as preliminary insights regarding the most common bottlenecks when learning Alloy (and Electrum). © Springer Nature Switzerland AG 2020.

Abstract
Software requirements engineers and testers generally define technical documents in natural languages, but this practice can lead to inconsistencies between the documentation and the consequent system implementation. Previous research has shown that writing requirements and tests in a structured way, with controlled natural languages like RSL, can help mitigate these problems. This study goes further, discussing new experiments carried out to validate that RSL (with its complementary tools, called “ITLingo Studio”) can be applied in different systems and technologies, namely the possibility of applying the approach to integrate test automation capabilities in security testing. The preliminary conclusion indicates that, by combining tools such as ITLingo Studio and the Robot Framework, it is possible to integrate requirements and test specifications with test automation, and that would bring benefits in the testing process’ productivity. © Springer Nature Switzerland AG 2020.

Abstract

Abstract
Reverse engineering may be helpful for extracting information from existing apps to understand them better and ease their maintenance. Reverse engineering may be performed by a static analysis of the apps’ code but, when the code is not available, a dynamic approach may be useful. This paper presents a tool that allows extracting dynamically, in a complete black-box approach, the explored activities of Android applications. It is an extension of iMPAcT testing tool that combines reverse engineering, dynamic exploration, and testing. The extracted information is later used to construct an HFSM (Hierarchical Finite State Machine) with three distinct levels of abstraction. The top-level shows the interactions needed to traverse the activities of the mobile application. The middle level shows the screens traversed while in a specific activity. The bottom level shows all screens traversed during exploration. This information helps to understand better the application which facilitates its maintenance and errors fixing. This paper provides a complete description of the tool, its architecture and the results of some case studies conducted on mobile apps publicly available on the Google Store. © Springer Nature Switzerland AG 2020.

Abstract
In today’s software industry, systems are constantly changing. To maintain their quality and to prevent failures at controlled costs is a challenge. One way to foster quality is through thorough and systematic testing. Therefore, the definition of adequate tests is crucial for saving time, cost and effort. This paper presents a framework that generates software test cases automatically based on user interaction data. We propose a data-driven software test generation solution that combines the use of frequent sequence mining and Markov chain modeling. We assess the quality of the generated test cases by empirically evaluating their coverage with respect to observed user interactions and code. We also measure the plausibility of the distribution of the events in the generated test sets using the Kullback-Leibler divergence. © 2020, Springer Nature Switzerland AG.

Abstract
Health literacy affects how people understand health information and, therefore, should be considered by search engines in health searches. In this work, we analyze how the level of health literacy is related to the eye movements of users searching the web for health information. We performed a user study with 30 participants that were asked to search online in the context of three work task situations defined by the authors. Their eye interactions with the Search Results Page and the Result Pages were logged using an eye-tracker and later analyzed. When searching online for health information, people with adequate health literacy spend more time and have more fixations on Search Result Pages. In this type of page, they also pay more attention to the results' hyperlink and snippet and click in more results too. In Result Pages, adequate health literacy users spend more time analyzing textual content than people with lower health literacy. We found statistical differences in terms of clicks, fixations, and time spent that could be used as a starting point for further research. That we know of, this is the first work to use an eye-tracker to explore how users with different health literacy search online for health-related information. As traditional instruments are too intrusive to be used by search engines, an automatic prediction of health literacy would be very useful for this type of system.