标题：
Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE
点击次数：
所属单位：
计算机科学与技术学院/人工智能学院/软件学院
发表刊物：
INTERNATIONAL JOURNAL OF AEROSPACE ENGINEERING
关键字：
MAST
摘要：
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.
ISSN号：
1687-5966
是否译文：
否
发表时间：
2018-01-01
合写作者：
Chen, Miaofang,朱
通讯作者：
王立松
发表时间：
2018-01-01
学位：工学博士学位
职称：教授
所在单位：计算机科学与技术/人工智能学院，公共实验教学部