Dependability Analysis for AADL Models by PVS

In recent years, architecture analysis & design language (AADL) has been applied to the development of dependable real-time systems, in which the quality of the developed software is an important factor. Thus, to make sure that real-time systems are really dependable, we must verify the important properties, such as safety and reliability. This paper describes a contribution to the transformation of AADL models. In this paper we present an approach for transforming AADL model into prototype verification system (PVS) specification and deductive verification of such AADL models using the PVS interactive theorem prover. Our transformation includes two aspects: structure and behavior description. Applying a PVS specification of a AADL language semantics, we generate a formal representation of the AADL model. After the transformation, some properties, such as safety and reliability, of the model build by AADL could be verified using PVS. We use an example to demonstrate the correctness and feasibility of our approach. Then, we verified the safety and reliability attributes of dependability in our model. At last, we conclude our paper by proposing that model transformation provides powerful support to improve the integration of formal verification in an industrial engineering process and we presented our future work direction.