Abstract
Although Finite-State Automata (FSA) have been successfully used in modeling and control of Discrete Event Systems (DESs), they are limited to represent complex and advanced features of DESs, such as context recognition and switching. The literature has suggested that a FSA can nevertheless be enriched with parameters properly collected from the modeled system, so that this favors design and control. A parameter can be embedded either on transitions or states. However, each approach is structured within a specific framework, so that their comparison and integration are not straightforward and they may lead to different control solutions, modeled, computed and implemented using distinct strategies. In this paper, we show how to combine advantages from parameters in modeling and control of DESs. Each approach is structured and their advantages are identified and exemplified. Then, we propose a conversion method that allows to translate a design-friendly model into a synthesis-efficient structure. Examples illustrate the approach.

Abstract
We construct functional encryption (FE) schemes for the orthogonality (OFE) relation where each ciphertext encrypts some vector (Formula Presented) and each decryption key, associated to some vector (Formula Presented), allows to determine if (Formula Presented) is orthogonal to (Formula Presented) or not. Motivated by compelling applications, we aim at schemes which are function hidding, i.e. (Formula Presented) is not leaked. Our main contribution are two such schemes, both rooted in existing constructions of FE for inner products (IPFE), i.e., where decryption keys reveal the inner product of (Formula Presented) and (Formula Presented). The first construction builds upon the very efficient IPFE by Kim et al. (SCN 2018) but just like the original scheme its security holds in the generic group model (GGM). The second scheme builds on recent developments in the construction of efficient IPFE schemes in the standard model and extends the work of Wee (TCC 2017) in leveraging these results for the construction of FE for Boolean functions. Conceptually, both our constructions can be seen as further evidence that shutting down leakage from inner product values to only a single bit for the orthogonality relation can be done with little overhead, not only in the GGM, but also in the standard model. We discuss potential applications of our constructions to secure databases and provide efficiency benchmarks. Our implementation shows that the first scheme is extremely fast and ready to be deployed in practical applications.

Abstract

Abstract

Abstract
The Robot Operating System (ROS) is one of the most popular open source robotic frameworks, and has contributed significantly to the fast development of robotics. Even though ROS provides many ready-made components, a robotic system is inherently complex, in particular regarding the architecture and orchestration of such components. Availability and analysis of a system's architecture at compile time is fundamental to ease comprehension and development of higher-quality software. However, ROS developers have to overcome this complexity relying mostly on testing and runtime visualisers. This work aims to enhance static-time support by proposing, firstly, a metamodel to describe the software architecture of ROS systems (the ROS Computation Graph) and, secondly, model extraction and visualisation tools for such architectural models. The provided tools allow users to specify custom-made queries over these models, enabling the static verification of relevant properties that had to be (manually) checked at runtime before.

Abstract
Formal modeling and automatic analysis are essential to achieve a trustworthy software design prior to its implementation. Alloy and its Analyzer are a popular language and tool for this task. Frequently, rather than a single software artifact, the goal is to develop a full software product line (SPL) with many variants supporting different features. Ideally, software design languages and tools should provide support for analyzing all such variants (e.g., by helping pinpoint combinations of features that could break a property), but that is not currently the case. Even when developing a single artifact, support for multi-variant analysis is desirable to explore design alternatives. Several techniques have been proposed to simplify the implementation of SPLs. One such technique is to use background colors to identify the fragments of code associated with each feature. In this paper we propose to use that same technique for formal design, showing how to add support for features and background colors to Alloy and its Analyzer, thus easing the analysis of software design variants. Some illustrative examples and evaluation results are presented, showing the benefits and efficiency of the implemented technique.