Extending Hybrid CSP with Probability and Stochasticity

TL;DR

This paper introduces a novel formal modeling language, SHCSP, extending Hybrid CSP with probabilistic and stochastic features, and develops an extended logic for reasoning about stochastic hybrid systems, addressing a key challenge in the field.

Contribution

It proposes a general compositional approach for modeling and verification of stochastic hybrid systems by extending Hybrid CSP and Hybrid Hoare Logic.

Findings

Successful extension of HCSP to include stochastic differential equations

Development of an extended logic for reasoning about SHCSP processes

Application demonstrated through a real-world example

Abstract

Probabilistic and stochastic behavior are omnipresent in computer controlled systems, in particular, so-called safety-critical hybrid systems, because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Tightly intertwining discrete, continuous and stochastic dynamics complicates modelling, analysis and verification of stochastic hybrid systems (SHSs). In the literature, this issue has been extensively investigated, but unfortunately it still remains challenging as no promising general solutions are available yet. In this paper, we give our effort by proposing a general compositional approach for modelling and verification of SHSs. First, we extend Hybrid CSP (HCSP), a very expressive and process algebra-like formal modeling language for hybrid systems, by introducing probability and stochasticity to model SHSs, which is called stochastic HCSP (SHCSP). To this end, ordinary differential equations (ODEs) are generalized by stochastic differential equations (SDEs) and non-deterministic choice is replaced by probabilistic choice. Then, we extend Hybrid Hoare Logic (HHL) to specify and reason about SHCSP processes. We demonstrate our approach by an example from real-world.