Modeling and analysing Cyber-Physical Systems in HOL-CSP

Modelling and Analysing Cyber-Physical Systems (CPS) is a challenge for Formal Methods and therefore a field of active research. It is characteristic of CPSs that models comprise aspects of Newtonian Physics appearing in system environments, the difficulties of their discretization, the problems of communication and interaction between actors in this environment as well as calculations respecting time-bounds. We present a novel framework to address these problems developed with industrial partners involved in the Autonomous Car domain. Based on HOL-CSP, we model time, physical evolution, "scenes"(global states) and "scenarios"(traces) as well as the interaction of "actors"(vehicles, pedestrians, traffic lights) inside this framework. In particular, discrete samplings are modelled by infinite internal choices.For several instances of the modelling framework, we give formal proofs of a particular safety property for Autonomous Cars: if each car follows the same driving strategy defined by the so-called Responsibility-Sensitive Safety (RSS), no collision will occur. The proofs give rise to a number of variants of RSS and optimizations as well as a test-case partitioning of abstract test cases and a test-strategy for integration tests.