Cyber-Physical Systems (CPS) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust, i.e., whether they are able to function correctly even in perturbed circumstances.

In this talk I will recap the achievements of my project on the development of a general formal framework and the tools necessary for the modelling, analysis and verification of CPS-like systems operating under uncertainty.

I will present the evolution sequence model for representing systems behaviour and the two temporal logics, RobTL and DisTL, introduced to specify robustness properties in various situations. I will also briefly introduce the “Software tool for the analsysis of robustness in the unkonw environment”, that includes a domain specific language for the specification of systems and their properties, and the model checkers for the two logics.