Abstract
This paper describes a methodology for task model design and analysis using the Alloy Analyzer, a formal, declarative modeling tool. Our methodology leverages (1) a formalization of the HAMSTERS task modeling notation in Alloy and (2) a method for encoding a concrete task model and compose it with a model of the interactive system. The Analyzer then automatically verifies the overall model against desired properties, revealing counter-examples (if any) in terms of interaction scenarios between the operator and the system. In addition, we demonstrate how Alloy can be used to encode various types of operator errors (e.g., inserting or omitting an action) into the base HAMSTERS model and generate erroneous interaction scenarios. Our methodology is applied to a task model describing the interaction of a traffic air controller with a semi-autonomous Arrival MANager (AMAN) planning tool.

Abstract
Robotic Process Automation (RPA) is a rules-based system for automating business processes by software bots that mimic human interactions to relieve employees from tedious work. It was verified in the literature that there are few works related to RPA decision support models. This technology is in great growth and, therefore, it becomes important to study the evaluation of the implementation of RPA. The objective of this work is focused on a literature review for the identification and analysis of Robotic Process Automation implementation models. This work analyses some models or studies available in the literature and, in addition, analyses it from a perspective relating to the Triple Bottom Line (TBL) related to environmental, social and economic effects. Regarding the results obtained, it appears that there is still a lot of room to improve research in this field, for example, with regard to the development of an evaluation model for the implementation of the RPA, taking into account the TBL of the sustainability concept.

Abstract
We approached the two-dimensional rectangular strip packing problem (2D-SPP), where the main goal is to pack a given number of rectangles without any overlap to minimize the height of the strip. Real-life constraints must be considered when developing 2D-SPP algorithms to deliver solutions that will improve the cutting processes. In the 2D-SPP literature, a gap related to studies approaching constraints in real-life scenarios was identified. Therefore, the impact of real-life constraints found in the plasma cutting process in sheet metal waste was analyzed. A mathematical model from the literature was modified to obtain packing arrangements with plasma cutting constraints. The combination of size and number of rectangles, as well as strip width, was the main factor that affected the packing arrangement, limiting the allocation of rectangles and generating empty spaces. In summary, considering the sheet metal waste context, instances with smaller widths should be avoided in practical operations for high minimum distance constraint values, returning the worst packing arrangements. For low minimum distance constraint values, smaller width instances can be used in practical operations, as the packing arrangement is acceptable. Finally, this article can reduce material waste and enhance the cutting process in the sheet metal industry, by showing packing characteristics which lead to higher amounts of raw material waste.

Abstract
A área de conhecimento associada à gestão de ativos potencia a extração de valor de ativos físicos, incorporando uma abordagem integrada que envolve riscos, custos e desempenho. Este trabalho propõe uma nova abordagem para selecionar projetos de investimento em infraestruturas no âmbito da gestão de ativos. A métrica padrão utilizada para a seleção de projetos em ativos múltiplos é o Índice de Valor de Infraestruturas (IVI), que tem sido utilizado para caracterizar ativos do setor de águas em diversos países. Este trabalho desenvolveu dois modelos de programação linear inteira mista. O primeiro modelo de otimização trata de um problema de alocação de orçamento de capital selecionando projetos de investimento com vista à maximização da condição dos ativos. O segundo modelo de otimização trata de um problema de planeamento de orçamento, visando minimizar o capital necessário para manter os ativos nas condições desejadas. A aplicação dos modelos é ilustrada por um estudo de caso de uma empresa que opera no setor da água em Portugal. Os resultados obtidos nos diferentes cenários analisados são discutidos com vista a apoiar o desenho de políticas de gestão de ativos mais eficientes.

Abstract
Task scheduling is a significant challenge in the cloud environment as it affects the network's performance regarding the workload of the cloud machines. It also directly impacts the consumed energy, therefore the profit of the cloud provider. This paper proposed an algorithm that prioritizes the tasks regarding their execution deadline. We also categorize the physical machines considering their configuration status. Henceforth, the proposed method assigns the jobs to the physical machines with the same priority class close to the user. Furthermore, we reduce the consumed energy of the machines processing the low-priority tasks using the DVFS method. The proposed method migrates the jobs to maintain the workload balance, or if the machines' class changed according to their scores. We have evaluated and validated the proposed method in the CloudSim library. The simulation results demonstrate that the proposed method optimized energy consumption by 12% and power consumption by 20%.

Abstract
Testing for infection with SARS-CoV-2 is an important intervention in reducing onwards transmission of COVID-19, particularly when combined with the isolation and contact-tracing of positive cases. Many countries with the capacity to do so have made use of lab-processed Polymerase Chain Reaction (PCR) testing targeted at individuals with symptoms and the contacts of confirmed cases. Alternatively, Lateral Flow Tests (LFTs) are able to deliver a result quickly, without lab-processing and at a relatively low cost. Their adoption can support regular mass asymptomatic testing, allowing earlier detection of infection and isolation of infectious individuals. In this paper we extend and apply the agent-based epidemic modelling framework Covasim to explore the impact of regular asymptomatic testing on the peak and total number of infections in an emerging COVID-19 wave. We explore testing with LFTs at different frequency levels within a population with high levels of immunity and with background symptomatic PCR testing, case isolation and contact tracing for testing. The effectiveness of regular asymptomatic testing was compared with ‘lockdown’ interventions seeking to reduce the number of non-household contacts across the whole population through measures such as mandating working from home and restrictions on gatherings. Since regular asymptomatic testing requires only those with a positive result to reduce contact, while lockdown measures require the whole population to reduce contact, any policy decision that seeks to trade off harms from infection against other harms will not automatically favour one over the other. Our results demonstrate that, where such a trade off is being made, at moderate rates of early exponential growth regular asymptomatic testing has the potential to achieve significant infection control without the wider harms associated with additional lockdown measures.