دورية أكاديمية
A FORMAL ANALYSIS FRAMEWORK FOR AADL
| العنوان: | A FORMAL ANALYSIS FRAMEWORK FOR AADL |
|---|---|
| المؤلفون: | Björnander, Stefan, Seceleanu, Cristina, Lundqvist, Kristina, Pettersson, Paul |
| المصدر: | Vietnam Journal of Science and Technology; Vol 49, No 5 (2011) ; Tạp chí Khoa học và Công nghệ; Vol 49, No 5 (2011) ; 2525-2518 |
| بيانات النشر: | Publishing House for Science and Technology |
| سنة النشر: | 2012 |
| المجموعة: | Vietnam Academy of Science and Technology: Journals Online |
| الوصف: | As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denota- tional semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL). |
| نوع الوثيقة: | article in journal/newspaper |
| وصف الملف: | application/pdf |
| اللغة: | Vietnamese |
| العلاقة: | http://vjs.ac.vn/index.php/jst/article/view/1896/2468Test; http://vjs.ac.vn/index.php/jst/article/view/1896Test |
| DOI: | 10.15625/0866-708X/49/5/1896 |
| الإتاحة: | https://doi.org/10.15625/0866-708X/49/5/1896Test http://vjs.ac.vn/index.php/jst/article/view/1896Test |
| رقم الانضمام: | edsbas.9DA40422 |
| قاعدة البيانات: | BASE |
| DOI: | 10.15625/0866-708X/49/5/1896 |
|---|