We consider the problem of estimating the numerical accuracy of programs with operations in fixed-point arithmetic and variables of arbitrary, mixed precision, and possibly non-deterministic value. By applying a set of parameterised rewrite rules, we transform the relevant fragments of the program under consideration into sequences of operations in integer arithmetic over vectors of bits, thereby reducing the problem as to whether the error enclosures in the initial program can ever exceed a given order of magnitude to simple reachability queries on the transformed program. We describe a possible verification flow and a prototype analyser that implements our technique. We present an experimental evaluation on a particularly complex industrial case study, including a preliminary comparison between bit-level and word-level decision procedures.

This paper presents a model of Satellite Base Station (SBS) networks subject to malicious attacks and defense actions. The SBS structure and the attack-defense actions are modelled as a two-player stochastic game and a Nash Equilibrium is computed to obtain the stationary strategy guaranteeing the best behaviour. On the basis of this result, the SBS dynamics are modelled as a Discrete Event System in a Timed Petri Net framework that allows obtaining the evolution of the SBS under the Nash Equilibrium and the stochastic game rules. A case study describing the cyber security of an SBS is outlined and the details of the model are illustrated.