Search

The communication network is a key component in parallel and distributed systems, high-performance computing (HPC) systems and Data Centers, as information exchange has a key role in communication-intensive applications. The all-to-all personalized exchange is a relevant communication pattern and has been extensively studied for many network topologies. When considering a Multistage Interconnection Network (MIN) with $\log N$ stages, the realization of all-to-all communication is obtained through a sequence of admissible permutations forming a Latin square. If a particular Latin square is desired, double MINs consisting of $2 \log N$ -1 stages are required. In this work, we consider the Butterfly-Butterfly network to realize the Latin square consisting of the identity permutation and its $N-1$ rotations, $\mathcal {RLS}$ , and we show how to obtain the sequence of rotations forming such a Latin square, without storing it. We propose a method to realize the $N$ permutations in pipeline fashion taking optimal $O(N)$ time, and we analyze the energy consumption according to the order of realization of the permutations, both on Butterfly-Butterfly network and on a single Butterfly used twice. We also show how to generate a Latin Square starting from any realizable permutation exploiting the switch configurations of the $\mathcal {RLS}$ .

A Sense and Respond (SaR) system endows a Business Intelligence system with the intelligence needed to react timely to exogenous as well as endogenous events. To this end, a SaR system needs to know the Key Performance Indicators (KPIs) that must be maximized as well as their relative weights. While the first information can be easily obtained through interviews, the second one is quite hard to get. This motivates the investigation of methods and tools to address this problem. In such a context, the main contributions of this paper are the following. First, we show how KPIs can be effectively defined using linear constraints. Second, we show how the problem of computing the actions that the SaR system proposes to the manager can be formulated as a Mixed Integer Linear Programming (MILP) problem. Third, we show how KPI weights can be computed from previous managing decisions by solving a suitable MILP problem. Fourth, we provide experimental results showing the effectiveness of the proposed approach.

In Boolean Network Tomography (BNT), node identifiability is a crucial property that reflects the possibility of unambiguously classifying the state of the nodes of a network as 'working' or 'failed' through end-to-end measurement paths. Designing a monitoring scheme satisfying network identifiability is an NP problem. In this article, we provide theoretical bounds on the minimum number of necessary measurement paths to guarantee identifiability of a given number of nodes. The bounds take into consideration two different classes of routing schemes (arbitrary and consistent routing) as well as quality of service (QoS) requirements. We formally prove the tightness of such bounds for the arbitrary routing scheme, and provide an algorithmic approach to the design of network topologies and path deployment that meet the discussed limits. Due to the computational complexity of the optimal solution, We evaluate the tightness of our lower bounds by comparing their values with an upper bound, obtained by a state-of-the-art heuristic for node identifiability. For our experiments we run extensive simulations on both synthetic and real network topologies, for which we show that the two bounds are close to each other, despite the fact that the provided lower bounds are topology agnostic.

The ever-increasing deployment of autonomous Cyber-Physical Systems (CPSs) (e.g., autonomous cars, UAV) exacerbates the need for efficient formal verification methods. In this setting, the main obstacle to overcome is the huge number of scenarios to be evaluated. Statistical Model Checking (SMC) is a simulation-based approach that holds the promise to overcome such an obstacle by using statistical methods in order to sample the set of scenarios. Many SMC tools exist, and they have been reviewed in several works. In this paper, we will overview Monte Carlo-based SMC tools in order to provide selection criteria based on Key Performance Indicators (KPIs) for the verification activity (e.g., minimize verification time or cost) as well as on the environment features, the kind of system model, the language used to define the requirements to be verified, the statistical inference approach used, and the algorithm implementing it. Furthermore, we will identify open research challenges in the field of (SMC) tools.

Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not formally modelled and the proof of correctness of the proposed approaches basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the system under verification. The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.