원문정보
보안공학연구지원센터(IJSEIA)
International Journal of Software Engineering and Its Applications
Vol.7 No.4
2013.07
pp.115-126
피인용수 : 0건 (자료제공 : 네이버학술정보)
초록
영어
The AADL is considered as one of the most powerful language for modeling the embedded systems. In this work, we propose an approach for the verification of the AADL architecture by using of the timed automata formalism. Indeed, the AADL architecture cannot be directly analyzed by model checking. An alternative for achieving that is to use the model driven engineering technology to extract an analysis model so that the properties can be verified using a model checker toolbox. The goal of this effort is to insure some properties of the AADL models using the Uppaal model checker. We show the application of our approach to an example.
목차
Abstract
1. Introduction
2. AADL: Presentation and Example
3. Preliminaries
4. Modeling Approach
4.1. The 1st step: Metamodelisation
4.2. The 2nd step: Process Transformation
4.3. The 3rd Step: Verification with the Uppaal
5. Uppaal Model Checker: An Overview
6. Applications
6.1. Verification with Uppaal Model Checker
7. Conclusion and Future Work
References
1. Introduction
2. AADL: Presentation and Example
3. Preliminaries
4. Modeling Approach
4.1. The 1st step: Metamodelisation
4.2. The 2nd step: Process Transformation
4.3. The 3rd Step: Verification with the Uppaal
5. Uppaal Model Checker: An Overview
6. Applications
6.1. Verification with Uppaal Model Checker
7. Conclusion and Future Work
References
저자정보
참고문헌
자료제공 : 네이버학술정보