Modelling And Verification Of Partition Operating System Based On Integrated Formal Method

The integrated modular avionics system has been widely used in safety-critical areas such as aircraft and aerospace.Its main goal is to implement a partitioned operating system,provide a resource sharing platform for multiple safety level subsystems as well as guarantee fault isolation and information flow control between applications using time separation and space separation.Due to the complexity of the partition operating system,its safety and reliability are difficult to guarantee through testing and simulation.A strict formal method is needed to establish a clear,unambiguous mathematical model and use mathematical reasoning and verification to guarantee its time separation and spatial separation capabilities.At present,the research on modeling and verification of partition operating systems mainly includes the use of theorem proving method to verify its spatial separation properties or the use of model checking methods to verify its time separation properties.There is a lacking of a unified framework to completely address the formal modeling and verification of time and space separation properties.This is mainly because the modeling language based on the theorem proving method usually cannot model the control flow and time of the system,nor can express the interactive behavior of concurrent objects.Conversely,the tools and languages used in model checking methods often lack a good stepwise refinement framework and are not good at the modeling and verification of data-intensive systems.In this thesis,based on the modeling and verification requirements of the partition operating system,an integrated formal method is proposed for the limitations of the theorem proof language Event-B and the model checking method LTS and timed automata.A framework based on the integrated formal method is provided for modeling and verification of the partition operating system,the behavior semantic model and time semantic model of Event-B is constructed.On this basis,the behavioral properties and time properties of the partition operating system are modeled and verified.The main work and innovation points of this thesis are as follows:(1)The problem of combined modelling using Event-B language and formal method based on model checking is studied,and a modelling and verification framework based on the integrated formal method for the partition operating system is proposed.In this thesis,a method of "mutual representation" is proposed for the limitations of Event-B and LTS,timed automata and other methods.The Event-B state machine is used to represent the modelling elements of LTS and timed automata.On this basis,a system modelling and verification framework combining Event-B and LTS /time automata is proposed,which provides a new idea for combining multiple formal methods to model and verify complex system.(2)The behavioural semantic model and temporal semantic model of Event-B modeling language are studied,and the correctness of these semantics model is proved.In this thesis,to deal with the limitations of Event-B language’s lacking behavioural semantics and temporal semantics,LTS is used to express the behavior semantics of Event-B,and time automaton is used to represent the temporal semantics of Event-B.The conversion rules from Event-B model to LTS model and timed automata model are presented,and the behavior equivalence of the Event-B model and its corresponding behavioural semantic model and temporal semantic model are proved by the bisimulation equivalence relation between LTS.Behaviour equivalence lays a theoretical foundation for the modelling and verification of the partition operating system using a combination of Event-B language and LTS and timed automata.(3)The stepwise refinement method of the model checking languages like LTS and timed automata are studied,and a stepwise refinement framework is provided.Traditional model checking methods often lack a stepwise refinement framework from abstract models to concrete models,which brings great difficulties to system modeling and analysis.In view of this drawback,this thesis draws on the stepwise refinement process of Event-B,and proposes a stepwise refinement framework of LTS and timed automata model.The framework summarizes the evolution process of the model into the decomposition of the behavior of an object in the vertical direction and the progressive addition of more concurrent objects in the horizontal direction,and propose various vertical refinement modes and horizontal expansion modes,which provides a new idea for the development of a multi-view integrated formal model.(4)Based on the above work,the behavior model and time model of the partitioned operating system are constructed,and the behavior porperties of it and schedulability are verified.Based on the above work,this thesis first uses the theorem proving language Event-B to construct the model of partition operating system specification ARINC 653 and translates it into an equivalent LTS model.The behaviour properties of Event-B model is guaranteed by verifying the corresponding behavior properties of the LTS model.Then,a two-level scheduling model of the partition operating system is built using Event-B and is converted into a corresponding time automaton model.The schedulability of the Event-B model is guaranteed by verifying the schedulability of the time automaton model.Through the construction and verification of the above two models,the practicability of the integrated formal method proposed in this thesis is proved.