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
Humans are good at understanding subjective or vague statements which, however, are hard to express in classical logic. Fuzzy logic is an evolution of classical logic that can cope with vague terms by handling degrees of truth and not just the crisp values true and false. Logic is the formal basis of computing, enabling the formal design of systems supported by tools such as model checkers and theorem provers.This paper shows how a model checker such as Alloy can evolve to handle both classical and fuzzy logic, enabling the specification of high-level quantitative relational models in the fuzzy domain. In particular, the paper showcases how QAlloy-F (a conservative, general-purpose quantitative extension to standard Alloy) can be used to tackle fuzzy problems, namely in the context of validating the design of fuzzy controllers. The evaluation of QAlloy-F against examples taken from various classes of fuzzy case studies shows the approach to be feasible.

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.