Formal Verification Techniques for Architecture-based Embedded Systems in EAST-ADL

Eun-Young Kang*

*Kontaktforfatter for dette arbejde

Publikation: Bog/antologi/afhandling/rapportRapportForskning

Resumé

Development of quality assured software-intensive systems, such as automotive embedded systems, is an increasing challenge as the complexity of these systems significantly increases. EAST-ADL is an architecture description language developed to specify automotive embedded system architectures at multiple abstraction levels in the development of safety-critical automotive products. In this paper, we propose an architecture-based verification technique which enhances the model-based development process supported by EAST-ADL by adapting model-checking to EAST-ADL specifications. We employ UPPAAL as a verification tool to ensure that predicted function behaviors of the models in EAST-ADL satisfy functional and real-time requirements. The criteria for this architecture-based verification is presented and the transformation rules which comply with this criteria are derived. This enables us to extract the relevant information from EAST-ADL specifications and to generate analyzable UPPAAL models. The formal semantics of EAST-ADL is defined which is essential to automate the verification of EAST-ADL specifications. Our approach is demonstrated by verifying the safety of the steering truck system units.
OriginalsprogEngelsk
ForlagarXiv
Antal sider19
StatusUdgivet - mar. 2019

Fingeraftryk

Embedded systems
Specifications
Model checking
Trucks
Computer systems
Semantics
Formal verification

Citer dette

@book{fb8c98667a7e430e9879d8306d17ea25,
title = "Formal Verification Techniques for Architecture-based Embedded Systems in EAST-ADL",
abstract = "Development of quality assured software-intensive systems, such as automotive embedded systems, is an increasing challenge as the complexity of these systems significantly increases. EAST-ADL is an architecture description language developed to specify automotive embedded system architectures at multiple abstraction levels in the development of safety-critical automotive products. In this paper, we propose an architecture-based verification technique which enhances the model-based development process supported by EAST-ADL by adapting model-checking to EAST-ADL specifications. We employ UPPAAL as a verification tool to ensure that predicted function behaviors of the models in EAST-ADL satisfy functional and real-time requirements. The criteria for this architecture-based verification is presented and the transformation rules which comply with this criteria are derived. This enables us to extract the relevant information from EAST-ADL specifications and to generate analyzable UPPAAL models. The formal semantics of EAST-ADL is defined which is essential to automate the verification of EAST-ADL specifications. Our approach is demonstrated by verifying the safety of the steering truck system units.",
author = "Eun-Young Kang",
year = "2019",
month = "3",
language = "English",
publisher = "arXiv",

}

Formal Verification Techniques for Architecture-based Embedded Systems in EAST-ADL. / Kang, Eun-Young.

arXiv, 2019. 19 s.

Publikation: Bog/antologi/afhandling/rapportRapportForskning

TY - RPRT

T1 - Formal Verification Techniques for Architecture-based Embedded Systems in EAST-ADL

AU - Kang, Eun-Young

PY - 2019/3

Y1 - 2019/3

N2 - Development of quality assured software-intensive systems, such as automotive embedded systems, is an increasing challenge as the complexity of these systems significantly increases. EAST-ADL is an architecture description language developed to specify automotive embedded system architectures at multiple abstraction levels in the development of safety-critical automotive products. In this paper, we propose an architecture-based verification technique which enhances the model-based development process supported by EAST-ADL by adapting model-checking to EAST-ADL specifications. We employ UPPAAL as a verification tool to ensure that predicted function behaviors of the models in EAST-ADL satisfy functional and real-time requirements. The criteria for this architecture-based verification is presented and the transformation rules which comply with this criteria are derived. This enables us to extract the relevant information from EAST-ADL specifications and to generate analyzable UPPAAL models. The formal semantics of EAST-ADL is defined which is essential to automate the verification of EAST-ADL specifications. Our approach is demonstrated by verifying the safety of the steering truck system units.

AB - Development of quality assured software-intensive systems, such as automotive embedded systems, is an increasing challenge as the complexity of these systems significantly increases. EAST-ADL is an architecture description language developed to specify automotive embedded system architectures at multiple abstraction levels in the development of safety-critical automotive products. In this paper, we propose an architecture-based verification technique which enhances the model-based development process supported by EAST-ADL by adapting model-checking to EAST-ADL specifications. We employ UPPAAL as a verification tool to ensure that predicted function behaviors of the models in EAST-ADL satisfy functional and real-time requirements. The criteria for this architecture-based verification is presented and the transformation rules which comply with this criteria are derived. This enables us to extract the relevant information from EAST-ADL specifications and to generate analyzable UPPAAL models. The formal semantics of EAST-ADL is defined which is essential to automate the verification of EAST-ADL specifications. Our approach is demonstrated by verifying the safety of the steering truck system units.

M3 - Report

BT - Formal Verification Techniques for Architecture-based Embedded Systems in EAST-ADL

PB - arXiv

ER -