Abstract
Payments using cryptocurrencies may require that the user is able to provide proof of ownership and proof of provenance for a specific transaction. In this paper an innovative web based solution is proposed as a framework that issues reports, on request, pertaining proof of ownership and proof of provenance. The proposed framework provides proof of ownership by using micro-payments and, when used recursively, it can produce provenance reports up to a defined granularity level of transactions. A proof of concept prototype of the proposed framework was implemented and its operation and output is presented and explained. Some limitations and future work directions are also identified. © The Editor(s) (if applicable) and The Author(s), under exclusive license to Springer Nature Switzerland AG 2020.

Abstract
Blood banks face inventory management problems associated to demand uncertainty and high inventory levels. An efficient blood inventory management is related to the use of simple, transparent and easy-to-understand procedures by blood banks’ employees. However, the literature about good practices in blood bank inventory management is scarce, reinforcing new developments need on this subject to ensure a good availability of blood products and reducing wastage. This research presents a blood inventory management system implemented in software, DOAR, able to meet demand while minimizing blood bags wastage. DOAR is simple, user-friendly and able to optimize blood inventory and donations. The purpose of the software is to provide a link between the demand by blood components and collected blood bags.

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 Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic. We explore different strategies to address variability, one in pure Electrum and another through an annotative language extension. We then show how Electrum 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 Electrum 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. © Springer Nature Switzerland AG 2020.

Abstract

Abstract
This paper presents Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances (including dynamic ones developed with the Electrum extension), to be used mainly in an educational context. By introducing secret paragraphs and commands in the models, Alloy4Fun allows the distribution and automated assessment of simple specification challenges, a mechanism that enables students to learn the language at their own pace. Alloy4Fun stores all versions of shared and analyzed models, as well as derivation trees that depict how they evolved over time: this wealth of information can be mined by researchers or tutors to identify, for example, learning breakdowns in the class or typical mistakes made by Alloy users. Alloy4Fun has been used in formal methods graduate courses for two years and for the latest edition we present results regarding its adoption by the students, as well as preliminary insights regarding the most common bottlenecks when learning Alloy (and Electrum). © Springer Nature Switzerland AG 2020.