Formal verification of dynamic and stochastic behaviors for automotive systems

Li Huang, Tian Liang, Eun Young Kang*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.

Original languageEnglish
Title of host publicationProceedings - 2019 24th International Conference on Engineering of Complex Computer Systems, ICECCS 2019
PublisherIEEE
Publication date2019
Pages11-20
ISBN (Print)9781728146478
ISBN (Electronic)9781728146461
DOIs
Publication statusPublished - 2019
Event24th International Conference on Engineering of Complex Computer Systems, ICECCS 2019 - Guangzhou, China
Duration: 10. Nov 201913. Nov 2019

Conference

Conference24th International Conference on Engineering of Complex Computer Systems, ICECCS 2019
Country/TerritoryChina
CityGuangzhou
Period10/11/201913/11/2019
SponsorDependable Intelligence, Institute of Intelligent Software

Keywords

  • Automotive Systems
  • PrCCSL
  • ProTL
  • UPPAAL-SMC

Fingerprint

Dive into the research topics of 'Formal verification of dynamic and stochastic behaviors for automotive systems'. Together they form a unique fingerprint.

Cite this