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

Abstract

Abstract
Ensuring the reproducibility of computational scientific experiments is crucial for advancing research and fostering scientific integrity. However, achieving reproducibility poses significant challenges, particularly in the absence of appropriate software tools to help. This paper addresses this issue by comparing existing tools designed to assist researchers across various fields in achieving reproducibility in their work. We were able to successfully run eight tools and execute them to reproduce three existing experiments from different domains. Our findings show the critical role of technical choices in shaping the capabilities of these tools for reproducibility efforts. By evaluating these tools for replicating experiments, we contribute insights into the current landscape of reproducibility support in scientific research. Our analysis offers guidance for researchers seeking appropriate tools to enhance the reproducibility of their experiments, highlighting the importance of informed technical decisions in facilitating reproducibility across diverse domains.

Abstract
User studies are paramount for advancing science. In particular, the empirical evaluation of programmer-oriented tools is important to validate research ideas and prototypes, as well as production-ready tools. Previous research has collected several tools used by the software engineering and behavioral science communities to design and run studies. In this work, we study tools used in software engineering studies and identify their features. Furthermore, we analyze three behavioral science experiment tools to identify design ideas that might be adapted to programmer user studies. With this work, we present the set of features currently offered by software engineering tools to support researchers in the design and execution of programmer user studies. We also present the characteristics of some tools used in behavioral science experiments to identify design ideas that can be adapted to programmer user studies.

Abstract