A Formal Verification Technique for Architecture-based Embedded Systems in EAST-ADL
This addresses the problem of ensuring safety and reliability in complex automotive embedded systems for developers and engineers, though it is incremental as it builds on existing EAST-ADL and UPPAAL tools.
The paper tackles the challenge of verifying safety-critical automotive embedded systems by proposing an architecture-based verification technique that adapts model-checking to EAST-ADL specifications, using UPPAAL to ensure functional and real-time requirements are satisfied, as demonstrated on a steering truck system.
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.