Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE
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...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2018-01-01
|
| Series: | International Journal of Aerospace Engineering |
| Online Access: | http://dx.doi.org/10.1155/2018/7019838 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832564342388686848 |
|---|---|
| author | Lisong Wang Miaofang Chen Jun Hu |
| author_facet | Lisong Wang Miaofang Chen Jun Hu |
| author_sort | Lisong Wang |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-8175497aba42425f99047ae6edfcc843 |
| institution | Kabale University |
| issn | 1687-5966 1687-5974 |
| language | English |
| publishDate | 2018-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | International Journal of Aerospace Engineering |
| spelling | doaj-art-8175497aba42425f99047ae6edfcc8432025-02-03T01:11:15ZengWileyInternational Journal of Aerospace Engineering1687-59661687-59742018-01-01201810.1155/2018/70198387019838Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTELisong Wang0Miaofang Chen1Jun Hu2College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, 29 Jiangjun Dadao, Nanjing 210016, ChinaCollege of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, 29 Jiangjun Dadao, Nanjing 210016, ChinaCollege of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, 29 Jiangjun Dadao, Nanjing 210016, ChinaThe 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.http://dx.doi.org/10.1155/2018/7019838 |
| spellingShingle | Lisong Wang Miaofang Chen Jun Hu Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE International Journal of Aerospace Engineering |
| title | Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE |
| title_full | Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE |
| title_fullStr | Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE |
| title_full_unstemmed | Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE |
| title_short | Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE |
| title_sort | formal verification method for configuration of integrated modular avionics system using marte |
| url | http://dx.doi.org/10.1155/2018/7019838 |
| work_keys_str_mv | AT lisongwang formalverificationmethodforconfigurationofintegratedmodularavionicssystemusingmarte AT miaofangchen formalverificationmethodforconfigurationofintegratedmodularavionicssystemusingmarte AT junhu formalverificationmethodforconfigurationofintegratedmodularavionicssystemusingmarte |