Abstract
This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach in which theoretical foundations and a practical tool are built together, as an alternative to foundations-first design (tool justifies theory) or tool-first design (foundations justify practice). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. We share two success stories of Caos' methodology and framework in our own teaching and research context, where we analyse a simple while-language and a choreographic language, including their operational rules and the concurrent composition of such rules. We further discuss how others can include Caos in their own analysis and Scala tools.

Abstract
Decent Work Agenda consists of a comprehensive initiative for promoting safety at work and social protection. Over 20 years since its conceptual release, measuring the progress of its elements is still challenging even after the publication of the decent work indicators guideline by the International Labour Organization in 2012. To close this gap, we use a Directional Distance Function (DDF) to measure the efficiency of safe work environment, and propose a combined measure taking into consideration also the efficacy. To illustrate the application of DDF in a reality-based case, we conducted a longitudinal study in a multinational organization. Data were collected from 21 branches of the company over 4 years (2018-2021). In the period of analysis, 60% of the branches were efficient in average, composing an overall efficiency score of 0.91. Our results also indicated low dispersion between the efficiency scores year on year due to a small-scale interquartile range. Finally, the use of efficiency combined with efficacy resulted in a promising approach for managerial applications. This research presents some contributions. One is the novelty approach of measuring the efficiency of safe work environment using a DDF model in a real-world application. Another is the managerial benefits of identifying benchmarks, as well as revealing potential improvements as a mechanism to reduce decent work deficits. From a modeling perspective, our conclusions suggest caution in considering only efficiency to measure safe work environment due to its relative nature. Thus, further studies are recommended to explore the use of combined measures in the analysis of decent work.

Abstract
The Brazilian Power System is mainly composed of renewable generation from hydroelectric and wind. Hence, spot and forward electricity prices tend to represent the inherently stochastic nature of these resources, while risk management is a measure taken by agents, especially hydro power plants (HPPs) to hedge against deep financial losses. A HPP goal is to maximize its profit considering uncertainties in forward electricity prices, spot prices, and generation scaling factor (GSF) for years ahead. Therefore, the objective of this work is to simulate the real decision-making process of a HPP, where they need to have a perspective of the forward market and future spot price assessment to negotiate forward electricity contracts. To do so, the present work models the uncertainty in electricity forward prices via two-stage stochastic programming, assessing the benefits of the stochastic solution in comparison to the deterministic one. In addition, different risk aversion levels are assessed using conditional value at risk (CVaR). An important conclusion is that the results show that the greater the HPP risk aversion is, the greater the energy selling via electricity forward contracts. Moreover, the proposed model has benefits in comparison to a deterministic approach.

Abstract
Photoplethysmography is a key sensing technology which is used in wearable devices such as smartwatches and fitness trackers. Currently, photoplethysmography sensors are used to monitor physiological parameters including heart rate and heart rhythm, and to track activities like sleep and exercise. Yet, wearable photoplethysmography has potential to provide much more information on health and wellbeing, which could inform clinical decision making. This Roadmap outlines directions for research and development to realise the full potential of wearable photoplethysmography. Experts discuss key topics within the areas of sensor design, signal processing, clinical applications, and research directions. Their perspectives provide valuable guidance to researchers developing wearable photoplethysmography technology.

Abstract
Nowadays global population and energy consumption and resources use are increasing, which means that the current consumption levels are unsustainable and a new approach for businesses of energy companies is required. This paper aims to conduct a systematic review of the literature about sustainable business models (SBM) in the energy sector. The main object of this study is to identify the current challenges and changes in business models in the energy sector to account for sustainability concerns. In this paper, 23 articles published in the last 5 years (Jan 2018 to Jun 2022) were selected and reviewed based on a meta-analysis. The articles were obtained from Scopus and Web of Science (WoS) databases departing from an appropriate set of keywords. The result of this study illustrates the importance of SBM in the energy sector and the important factors considered in their development.

Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.