Research On Formal Verification Of Embedded Software Based On

In order to satisfy the avionics system software requirements, for example, high reliability, in1997, American Air-lines Electronic Engineering Committee (AEEC) released the avionics system application software interface standard (ARINC653standard). Currently, ARINC653have been developed for the main industry standard, it defines a series of functions used in the avionics system design. But ARINC653just give related standard, did not give relevant concepts of abstract symbols. As a result, in2011, the SAE released ARINC653attachment used to describe ARINC653standard, and as a Model Driven (Model Driven Architecture, MDA) in the field of outstanding person AADL can not only describe the embedded hardware and software structure, and to verify the embedded software related non-functional attributes.But in practice, ARINC653attachment is only through natural language describes the related mapping relationship. For developers, this can easily cause misunderstanding and produce ambiguity, and it not a explicitly mechanism to perform the related constraint checking defects, then easily lead to developers in modeling violated ARINC653standard potential field constraint. Although ARINC653standard stipulated in the two layers of scheduling mechanism, but does not give the corresponding partition design standards. Its based on time slice rotation scheduling algorithm is given, although simple, but often produce free partition, lead to the waste of resources. And at the same time, the complexity of the software also brought the problem of software reliability, but based on AADL ARINC653error model can only be expressed as a static model of the system, for the dynamic behavior of the between components in the reliability model, it brings inconvenience. Therefore, for the above problems, this paper made the following research:First, this paper divides the ARINC653software for partitioning model, task partition model and error model, using mathematical definition describes the model of ARINC653standards defined by the related elements and AADL standards defined in the relationship between elements. And use Requirements Enforcement Analysis Language (REAL) to perform ARINC653field constraint checking model, so as to avoid inconsistent constraint model and the field. Then, gived based on weighted rotary ARINC653scheduling strategy, defined partition weight calculation formula. Partition based on weighted cycle, and RMS scheduling algorithm as partition-inside scheduling. And the AADL open source integrated development environment (OSATE) for secondary development to support two layers of scheduling, so it can analysis the scheduling policy.Finally, based on AADL ARINC653error model can only be expressed as a static model of the system, in order to better evaluate the reliability of the models based on AADL ARINC653, from the basic concept of error, error, error of the spread of the filter/block into consideration, puts forward relevant transformation rules, convert the ARINC653model based on AADL to generalized stochastic Petri nets. And based on stochastic petri nets analysis techniques evaluate reliability.