Verification Based Development Process for Embedded Systems

International audienceDesigning safety critical systems is a complex task due to the need of guaranteeing that the resulting model can cope with all the functional and non-functional requirements of the system. Obtaining such guarantees is only possible with the use of model verification techniques. This paper presents an approach aimed to fulfill the needs of critical system design. The proposed approach is based on the Architecture Analysis and Design Language (AADL), which is suitable to describe the system’s architecture. It contains a sequence of model transformations that easies the verification of the designed AADL model and so assures its correctness. It must be highlighted that this is not performed in a single step, as it is possible to verify AADL models with different abstrac- tion levels, which allows successive refinements in a top-down approach. We use a case study from an Au- tonomous Parking System to illustrate the proposed development process