Translating EAST-ADL/Stateflow Models into Probabilistic Verifiable Models: Statistical Verification of Vehicle Systems in EAST-ADL/Stateflow using UPPAAL Tools

Eun-Young Kang*, Jianda Chen, Liu Ke, Shangyu Chen

*Corresponding author for this work

Research output: Book/anthology/thesis/reportReportResearch

Abstract

EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time be-havioral constraints in EAST-ADL into analyzable UPPAAL models. In this paper, we extend our previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models with stochastic semantics and integrating the translation with formal statistical analysis techniques: a flattening strategy and a set of mapping rules are proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on automotive and quadcopter case studies.
Original languageEnglish
Number of pages51
Publication statusPublished - Mar 2019

Fingerprint

Embedded systems
Statistical methods
Semantics
Systems analysis
Statistical Models
Formal verification

Cite this

@book{ac17e5e0096544e9b55a8ae1624f5aba,
title = "Translating EAST-ADL/Stateflow Models into Probabilistic Verifiable Models: Statistical Verification of Vehicle Systems in EAST-ADL/Stateflow using UPPAAL Tools",
abstract = "EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time be-havioral constraints in EAST-ADL into analyzable UPPAAL models. In this paper, we extend our previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models with stochastic semantics and integrating the translation with formal statistical analysis techniques: a flattening strategy and a set of mapping rules are proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on automotive and quadcopter case studies.",
author = "Eun-Young Kang and Jianda Chen and Liu Ke and Shangyu Chen",
year = "2019",
month = "3",
language = "English",

}

Translating EAST-ADL/Stateflow Models into Probabilistic Verifiable Models: Statistical Verification of Vehicle Systems in EAST-ADL/Stateflow using UPPAAL Tools. / Kang, Eun-Young; Chen, Jianda; Ke, Liu; Chen, Shangyu.

2019. 51 p.

Research output: Book/anthology/thesis/reportReportResearch

TY - RPRT

T1 - Translating EAST-ADL/Stateflow Models into Probabilistic Verifiable Models: Statistical Verification of Vehicle Systems in EAST-ADL/Stateflow using UPPAAL Tools

AU - Kang, Eun-Young

AU - Chen, Jianda

AU - Ke, Liu

AU - Chen, Shangyu

PY - 2019/3

Y1 - 2019/3

N2 - EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time be-havioral constraints in EAST-ADL into analyzable UPPAAL models. In this paper, we extend our previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models with stochastic semantics and integrating the translation with formal statistical analysis techniques: a flattening strategy and a set of mapping rules are proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on automotive and quadcopter case studies.

AB - EAST-ADL is an architectural description language dedicated to safety-critical automotive embedded system design. We have previously modified EAST-ADL to include energy constraints and transformed energy-aware real-time be-havioral constraints in EAST-ADL into analyzable UPPAAL models. In this paper, we extend our previous work by including support for Stateflow, which is used to design event-driven systems via hierarchical state machines and flow charts. However, Stateflow provides limited support for formal analysis and often suffers from incomplete coverage issues since it was originally designed for the simulation of designs and as such does not provide a model amenable to formal verification. We tackle that shortcoming by transforming Stateflow models into verifiable UPPAAL models with stochastic semantics and integrating the translation with formal statistical analysis techniques: a flattening strategy and a set of mapping rules are proposed to facilitate the guarantee of translation. Furthermore, a set of mapping rules is presented to ensure the translation is correct, efficient, and applicable to real case studies. The analysis techniques, including the flattening and mapping strategy, are validated and demonstrated on automotive and quadcopter case studies.

M3 - Report

BT - Translating EAST-ADL/Stateflow Models into Probabilistic Verifiable Models: Statistical Verification of Vehicle Systems in EAST-ADL/Stateflow using UPPAAL Tools

ER -