Tool-Supported Analysis of Dynamic and Stochastic Behaviors in Cyber-Physical Systems

Formal analysis of functional and non-functional requirements is crucial in cyber-physical systems (CPS), in which controllers interact with physical environments. The continuous time behaviors of CPS often rely on complex dynamics as well as on stochastic behaviors. We have previously proposed a probabilistic extension of Clock Constraint Specification Language, called PrCCSL, for specification of (non)-functional requirements of CPS and proved the correctness of requirements by mapping the semantics of the specifications into verifiable UPPAAL models. Previous work is extended in this paper by including an extension of PrCCSL, i.e., PrCCSL*, which incorporates annotations of continuous behaviors and stochastic characteristics of CPS. The CPS behaviors are specified in PrCCSL* and translated into stochastic UPPAAL models for formal verification. The translation algorithm from PrCCSL* into UPPAAL models is provided and implemented in an automatic translation tool, namely ProTL. Formal verification of CPS against (non)-functional requirements is performed by ProTL using UPPAAL-SMC as an analysis backend. Our approach is demonstrated on a series of CPS case studies.