Research On Verification Technology Of Embedded Software System Based On

With the rapid development of embedded systems, the structure of systems also will be more complex, especially in avionics systems, it has developed into an integrated modular system. At the same time, requirements for the security and reliability of the system and other non-functional property are also increasing. To meet this demand, American Airlines Electronic Engineering Association released ARINC653 standard in 1997, the avionics system application software interface standard. After years of development, it has become a major industry standard of avionics systems. But ARINC653 just gives the relevant standards, and did not give express concepts of abstract symbols. Thus, the American Society of Automotive Engineers released ARINC653 annex based on AADL in 2011,and described ARINC653 standard by that. With the help of multiple annexes, AADL can describe not only the hardware and software architecture for embedded systems, and can analyze the non-functional properties of embedded systems.Although ARINC653 standard provides double levels scheduling mechanism, but did not give the appropriate partition design standards, And though the scheduling algorithm based on rotation of the main time frame is easy to understand,but there is a defects of wasting idle time. In addition, the complexity of the software has also brought problems of software reliability. While AADL error model can described reliability problem with the system, but it can only be expressed as a static model, it is difficult to model the dynamic interactions between components in reliability model of system. Because of the problems raised above, This paper studies the problem of the following areas:(1) First,The priority-based partition scheduling mechanism is applied to ARINC653 software. Since priority-based partition scheduling mechanism allows multiple partition that preemptive idle time of main time frame,thus it can compensate the defect of wasting idle time in ARINC653 standard. Secondly, in order to analyse the schedulability of priority-based partition scheduling mechanism partition used in this paper, this paper improved AADL open source integrated development environment (OSATE) to support double level scheduling mechanism.(2) AADL error model has only a static description for the system’s flaws, In order to better analyze the reliability of the model,this paper consider various aspects of the error model,such as basic concept,error propagation and error filtering,than put forward the relevant conversion rules,transformating the AADL reliability model into fault tree, And verify the reliability of the software based on existing fault tree.(3) Verify the schedulability and reliability of flight planning subsystem based on Open-source Integrated Development Environment (OSATE). The results show that priority-based partition scheduling mechanism can compensate the defect of wasting idle time of ARINC653 standard’s scheduling mechanism, and the method that transformate the reliability model to fault tree can effectively evaluate the reliability of the system.