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.

Abstract
The architecture for 5G core includes a Service-Based Architecture for the diverse network functions (NFs), which relies on HTTP/2 for the SBI and TCP as the underlying transport protocol. The specifications of the HTTP family is moving towards more efficient and secure protocols, which are based on UDP to assure enhanced transport but using TLS to secure the communication channel. The next generation of microservices needs to be more secure, performant and easily manageable, where HTTP/3 and containers orchestration platforms (like Kubernetes) can provide significative contributions towards such goals. Different deployment approaches can be followed for services implemented in compliance to the 5G SBA. This paper contributes with the assessment of deployment models for services in 5G networks, where NFs are implemented following traditional architectures (all the functions in a VM) or as serverless architectures (with functions distributed in containers). The performance of microservices in Kubernetes is also evaluated. The evaluation conducted also considers the employment of different versions of HTTPs to empower the service-based interfaces of 5G services. Results demonstrate performance benefits of employing HTTP/3, based on QUIC protocol, in scenarios with networks characterised by losses or delay conditions. Despite such gain, deployment in 5G networks needs to carefully consider aspects related with connection tracking mechanisms to support high volumes of requests.

Abstract
The media sector is constantly evolving and, in the last few years, such evolution has been driven by a number of convergence paradigms, notably, that between broadband and broadcast technologies with the introduction of IT and IP technology. The present trend is to switch totally from a closed niche that uses highly specialized equipment to off-the-shelf IT-centric solutions, offering easy configuration and remote operation. The aim is to enable common computers to be turned into highly capable media devices and act as connected objects adopting an IoT-like paradigm. This vision, though, is not implemented easily, given that most media industry professionals do not yet feel comfortable operating in the IT technology space and also due to the stringent requirements that exist in this industry. The Joint Task Force on Networked Media is defining specifications that aim at overcoming such existing barriers. In this article we present a novel solution that follows the guidelines delivered by this group to set up a remotely operated media production facility, totally based on IP and IT technology, constituting a step forward the realization of the IoT concept in professional media environments. The focus is on two complementary components, namely, the GUI Agent and the MW Agent, which are not covered by the defined specifications but that are crucial to speed up the deployment of concrete solutions that can be easily operated by non-IT and non-IP experts in a transparent and ubiquitous way. © 2020 TRON Forum.