Boolean network tomography is a powerful tool to infer the state (working/failed) of individual nodes from path-level measurements obtained by edge-nodes. We consider the problem of optimizing the capability of identifying network failures through the design of monitoring schemes. Finding an optimal solution is NP-hard and a large body of work has been devoted to heuristic approaches providing lower bounds. Unlike previous works, we provide upper bounds on the maximum number of identifiable nodes, given the number of monitoring paths and different constraints on the network topology, the routing scheme, and the maximum path length. These upper bounds represent a fundamental limit on identifiability of failures via Boolean network tomography. Our analysis provides insights on how to design topologies and related monitoring schemes to achieve the maximum identifiability under various network settings. Through analysis and experiments we demonstrate the tightness of the bounds and efficacy of the design insights for engineered as well as real networks.

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.

Boolean Network Tomography (BNT) aims at identifying failures of internal network components by means of end-to-end monitoring paths. However, when the number of failures is not known a priori, failure identification may require a huge number of monitoring paths. We address this problem by designing a Bayesian approach that progressively selects the next path to probe on the basis of its expected information utility, conditioned on prior observations. As the complexity of the computation of posterior probabilities of node failures is exponential in the number of failed paths, we propose a polynomial-time greedy strategy which approximates these values. To consider aging of information in dynamic failure scenarios where node states can change during a monitoring period, we propose a monitoring technique based on a sliding observation window of adaptive length. By means of numerical experiments conducted on real network topologies we demonstrate the practical applicability of our approach, and the superiority of our algorithms with respect to state of the art solutions based on classic BNT as well as sequential group testing.