# A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL

## TL;DR

This paper introduces a formal verification method that integrates model-checking with EAST-ADL specifications for automotive embedded systems, ensuring safety and correctness at multiple abstraction levels.

## Contribution

It develops a formal semantics for EAST-ADL and a transformation process to generate UPPAAL models for automated verification of system requirements.

## Key findings

- Successful verification of steering truck system units.
- Enhanced model-based development with formal safety guarantees.
- Automated extraction of verification models from EAST-ADL specifications.

## 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.