![](/images/graphics-bg.png)
Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE
المؤلفون المشاركون
Wang, Lisong
Chen, Miaofang
Hu, Jun
المصدر
International Journal of Aerospace Engineering
العدد
المجلد 2018، العدد 2018 (31 ديسمبر/كانون الأول 2018)، ص ص. 1-22، 22ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2018-04-22
دولة النشر
مصر
عدد الصفحات
22
الملخص EN
The configuration information of Integrated Modular Avionics (IMA) system includes almost all details of whole system architecture, which is used to configure the hardware interfaces, operating system, and interactions among applications to make an IMA system work correctly and reliably.
It is very important to ensure the correctness and integrity of the configuration in the IMA system design phase.
In this paper, we focus on modelling and verification of configuration information of IMA/ARINC653 system based on MARTE (Modelling and Analysis for Real-time and Embedded Systems).
Firstly, we define semantic mapping from key concepts of configuration (such as modules, partitions, memory, process, and communications) to components of MARTE element and propose a method for model transformation between XML-formatted configuration information and MARTE models.
Then we present a formal verification framework for ARINC653 system configuration based on theorem proof techniques, including construction of corresponding REAL theorems according to the semantics of those key components of configuration information and formal verification of theorems for the properties of IMA, such as time constraints, spatial isolation, and health monitoring.
After that, a special issue of schedulability analysis of ARINC653 system is studied.
We design a hierarchical scheduling strategy with consideration of characters of the ARINC653 system, and a scheduling analyzer MAST-2 is used to implement hierarchical schedule analysis.
Lastly, we design a prototype tool, called Configuration Checker for ARINC653 (CC653), and two case studies show that the methods proposed in this paper are feasible and efficient.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Wang, Lisong& Chen, Miaofang& Hu, Jun. 2018. Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE. International Journal of Aerospace Engineering،Vol. 2018, no. 2018, pp.1-22.
https://search.emarefa.net/detail/BIM-1167635
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Wang, Lisong…[et al.]. Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE. International Journal of Aerospace Engineering No. 2018 (2018), pp.1-22.
https://search.emarefa.net/detail/BIM-1167635
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Wang, Lisong& Chen, Miaofang& Hu, Jun. Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE. International Journal of Aerospace Engineering. 2018. Vol. 2018, no. 2018, pp.1-22.
https://search.emarefa.net/detail/BIM-1167635
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-1167635
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
![](/images/ebook-kashef.png)
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر
![](/images/kashef-image.png)