Abstract

Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

Abstract
Data description is a fundamental step in Research Data Management (RDM). When it comes to images, the challenge is increased, as they have characteristics that differentiate them from other typologies. We conducted a study in which we obtained a set of 27 images described according to their content, by researchers of the projects where they are inserted. After obtaining the ground-truth that would support the analysis, we proceeded to two more stages of description, one through an automatic processing tool (Vision AI) and the other through researchers with no knowledge of the images. We concluded that the human description is more elucidative of the images' content, namely at a semantic level. In turn, the automatic tools enhance a more literal description. This study allowed us to reflect on the description of images in a research context and to discuss the potential of formal analysis and analysis of the semantic expression of images.

Abstract
Ensuring privacy while sharing sensitive data is critical, particularly in fields such as healthcare, and everywhere compliance with data protection regulations is required. Anonymization and pseudonymization techniques are essential for preserving individual privacy but it is challenging to select the most appropriate methods given particular privacy and utility requirements. We conducted a focus group during the EuroPLoP 2024 conference that aimed to obtain feedback on patterns that we documented in this space and on a pattern map we outlined, and to identify patterns related to anonymization or pseudonymization of data that have not yet been documented. Some of the patterns we documented were not known by participants. On the other hand, we found some techniques that are potentially privacy-preserving patterns that have not yet been documented, and framed these techniques according to the category in our pattern map. Although the results suggest that our current patterns address some recurring privacy challenges, further exploration and documentation of the techniques are necessary to capture the full range of privacy-preserving solutions.

Abstract

Abstract
Advancements in the energy efficiency and computational power of embedded devices allow developers to equip resource-constrained systems with a greater number of features and more complex behavior. As complexity of a system grows, so does the difficulty in demonstrating its overall correctness. Formal methods have been successfully applied in a variety of verification and validation scenarios, but their wide adoption in the industry and academia is still lackluster. Among the explanations listed in the literature for the low adoption of these techniques are the perceived difficulty of getting into formal practices and how formal tools are not usually aimed at practical use cases. Striving to address these issues, we present MARS, an open-source domain-specific language for the safe instrumentation of runtime verification monitors into real-time resource-constrained distributed systems. Our main objective with MARS is to ease the integration of runtime verification monitors in distributed applications while also providing developers with evidence of their correct instrumentation in the context of systems where dependability and temporal requirements need to be respected even under extreme resource constraints. We present the language syntax, the set of tools embedded into its compiler, its functionalities, and a use case to exemplify its use in a practical distributed application. © 2024 IEEE.