A refinement approach to analyse critical cyber-physical systems. Extended Version

Cyber-Physical Systems (CPS) are characterised by digital components controlling physical equipment, and CPS are typically influenced by the surrounding environment conditions. Due to the stochastic continuous nature of the involved physical phenomena, for quantitative evaluation of non-functional properties (e.g. dependability, performance) stochastic hybrid model-based approaches are mainly used. In case of critical applications, it is also important to verify specific qualitative aspects (e.g. safety). Generally, stochastic hybrid approaches are not suitable to account for the co-existence of both qualitative and quantitative aspects. In this paper we address this issue by proposing a refinement approach for analysing stochastic hybrid systems starting from a verified discrete representation of their logic. Different formalisms are used and formally related. It is then possible to combine the quantitative assessment of stochastic continuous properties with the qualitative verification of logic soundness, thus improving the trustworthiness of the analysis results.