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. |
Year | Venue | DocType |
---|---|---|
2019 | arXiv: Software Engineering | Journal |
Volume | Citations | PageRank |
abs/1903.06241 | 0 | 0.34 |
References | Authors | |
0 | 1 |
Name | Order | Citations | PageRank |
---|---|---|---|
Eun-Young Kang | 1 | 2 | 1.73 |