Abstract

Abstract
Motor controllers, such as the ones used in signalling systems, include critical embedded software. Alstom is a company that produces such embedded systems, which must follow complex certification processes that require formal modelling and analysis. The formal analysis of these real-time systems have to balance between including enough details to be useful and abstracting away enough details to be verifiable. This paper describes our work in the context of the European VALU3S project to integrate the analysis of such systems with the Uppaal model checker during the development cycle, involving both developers from Alstom and academic partners. We use special Excel tables to configure the underlying Uppaal models and requirements, bridging these two stakeholders. We follow Software Product Line Engineering principles, e.g., allowing features to be turned on and off and periodicities to be changed, and verify different properties for each of such configuration. We automate the instantiation and verification in Uppaal of a set of selected configurations via an open-source prototype tool named Uppex.

Abstract

Abstract
The increasing number of IoT devices and digital services offers cross-domain sensing and control opportunities to a growing set of stakeholders. The provision of cross-domain digital services requires interoperability as a key enabler to bridge domain specifics, while inferring knowledge and allowing new data-driven services. This work addresses H2020 InterConnect project's Interoperability Framework, highlighting the use of semantic web technologies. The interoperability framework layering is presented, particularly addressing the Semantic Interoperability layer as its cornerstone to build an interoperable ecosystem of cross-domain digital services via a federation of distributed knowledge bases. Departing from a generic, ontology-agnostic approach that can fit any cross-domain use case, it validates the approach by considering the SAREF family of ontologies, showcasing an IoT and energy cross-domain use case.

Abstract
Nowadays, manufacturing companies present complex and robust in-house logistics operations that support production lines, where high system efficiency is the primary goal. However, to achieve the desired degree of efficiency, the use of tools that can help decision-makers to identify the improved set of operations is required. This need is explored in this work through the development of a simulation model. The model is inspired by a real automotive plant, where a segment of a mixed-model assembly line composed by a supermarket, diverse kits, human pickers and automated guided vehicles (AGV) is explored. Different scenarios are studied to analyse the potential for production support operation improvement, where the introduction of automated technologies, like robots, is explored. Results show that the system, through the addition of intelligent dynamic carrier robots, can significantly improve efficiency while reducing resources deployed. Furthermore, sizing the human workforce at the supermarket is the key to having a well-balanced production system.

Abstract
The prevalence and availability of cloud infrastructures has made them the de facto solution for storing and archiving data, both for organizations and individual users. Nonetheless, the cloud's wide spread adoption is still hindered by dependability and security concerns, particularly in applications with large data collections where efficient search and retrieval services are also major requirements. This leads to an increased tension between security, efficiency, and search expressiveness. In this article we tackle this tension by proposing BISEN, a new provably-secure boolean searchable symmetric encryption scheme that improves these three complementary dimensions by exploring the design space of isolation guarantees offered by novel commodity hardware such as Intel SGX, abstracted as Isolated Execution Environments (IEEs). BISEN is the first scheme to support multiple users and enable highly expressive and arbitrarily complex boolean queries, with minimal information leakage regarding performed queries and accessed data, and verifiability regarding fully malicious adversaries. Furthermore, BISEN extends the traditional SSE model to support filter functions on search results based on generic metadata created by the users. Experimental validation and comparison with the state of art shows that BISEN provides better performance with enriched search semantics and security properties.