ARINC653 systems, which have been widely used in avionics industry, are an important class of safety-critical applications. Partitions are the core concept in the Arinc653 system architecture. Due to the existence of ...ARINC653 systems, which have been widely used in avionics industry, are an important class of safety-critical applications. Partitions are the core concept in the Arinc653 system architecture. Due to the existence of partitions, the system designer must allocate adequate time slots statically to each partition in the design phase. Although some time slot allocation policies could be borrowed from task scheduling policies, no existing literatures give an optimal allocation policy. In this paper, we present a partition configuration policy and prove that this policy is optimal in the sense that if this policy fails to configure adequate time slots to each partition, nor do other policies. Then, by simulation, we show the effects of different partition configuration policies on time slot allocation of partitions and task response time, respectively.展开更多
针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方...针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建模仿真,并结合统计模型检验(Statistical Model Checking,SMC)与符号模型检验(Symbolic Model Checking,MC)来验证其可调度性。实验结果表明,该方法不仅快速验证了IMA系统的可调度性,而且能够准确定位不可调度任务。展开更多
基金supported by the National Natural Science Foundation of China under Grant No. 90718019the National High-Tech Research and Development Plan of China under Grant No. 2007AA010304
文摘ARINC653 systems, which have been widely used in avionics industry, are an important class of safety-critical applications. Partitions are the core concept in the Arinc653 system architecture. Due to the existence of partitions, the system designer must allocate adequate time slots statically to each partition in the design phase. Although some time slot allocation policies could be borrowed from task scheduling policies, no existing literatures give an optimal allocation policy. In this paper, we present a partition configuration policy and prove that this policy is optimal in the sense that if this policy fails to configure adequate time slots to each partition, nor do other policies. Then, by simulation, we show the effects of different partition configuration policies on time slot allocation of partitions and task response time, respectively.
文摘针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建模仿真,并结合统计模型检验(Statistical Model Checking,SMC)与符号模型检验(Symbolic Model Checking,MC)来验证其可调度性。实验结果表明,该方法不仅快速验证了IMA系统的可调度性,而且能够准确定位不可调度任务。
