Consistency Preserving Development of Embedded Systems Using AADL

T. Szmuc, W. Szmuc (AGH Univ. of Science and Techn., Poland)

The goal of the paper is to present and analyze main AADL features enabling systematic verification of properties and preserving consistency of developed artefacts. Scope of the analysis is ranged not only to existing AADL based tools but also an application of Colored Petri Nets for modelling and verification is proposed. Systematic design and verification case study is presented in the paper. The study starts with a definition of general system structure using AADL textual language. In the first step, the description focuses on block structure, i.e. blocks with interfaces and connections. Devices which specify the environment of the system are also defined. In the next steps, the general structure is refined by definition of internal structures, hardware elements, time parameters and scheduling modes. Verification of time requirements (latency, time for specified paths etc.) are verified for the defined system. The next step is safety analysis which needs the previous definition of error levels and error possible flows through architecture. The system designed The above mentioned activities allow to design system structure correct with regard to specified time safety parameters. The system frames may be then injected by C/C++, Ada and Java code. The development may be also supported by formal modelling and verification. Translation rules of main AADL structure into Colored Petri nets and possibilities for merging formal verification with AADL development process are also presented.