Formal Verification of Dynamic and Stochastic Behaviors for Automotive Systems

TL;DR

This paper introduces PrCCSL*, an extension of a formal specification language, enabling the verification of complex stochastic and dynamic behaviors in automotive systems through automated translation and analysis tools.

Contribution

We extend PrCCSL to PrCCSL* for modeling stochastic and dynamic behaviors, and develop ProTL for automatic translation and verification using UPPAAL-SMC.

Findings

Successfully modeled complex behaviors in automotive systems

Automated translation enables efficient formal verification

Validated approach on two real-world automotive case studies

Abstract

Formal analysis of functional and non-functional requirements is crucial in automotive systems. The behaviors of those systems often rely on complex dynamics as well as on stochastic behaviors. We have proposed a probabilistic extension of Clock Constraint Specification Language, called PrCCSL,for specification of (non)-functional requirements and proved the correctness of requirements by mapping the semantics of the specifications into UPPAAL models. Previous work is extended in this paper by including an extension of PrCCSL, called PrCCSL*, for specification of stochastic and dynamic system behaviors, as well as complex requirements related to multiple events. To formally analyze the system behaviors/requirements specified in PrCCSL*, the PrCCSL* specifications are translated into stochastic UPPAAL models for formal verification. We implement an automatic translation tool, namely ProTL, which can also perform formal analysis on PrCCSL* specifications using UPPAAL-SMC as an analysis backend. Our approach is demonstrated on two automotive systems case studies.