Model checking real-time software system based on a new interface interaautomata with intense constrains

Components in software system usually interact with the environment by increasing complex interfaces to bring more possible failures with the increasing system scale, it has been becoming important to describe and verify the component properties by some formal methods at the interface level to guarantee its quality and reliability. Due to the weak or simplified multidimensional constraints specified between these different interfaces, the influence of performance, efficiency and sufficiency for the current interface automata based testing and verification is great, especially model checking with strict requirements of state space. To solve these challenges, we proposed a new defined interface interaction automata (IIA) to model the specification of the complex interaction process between input and output interfaces, including graphical value, temporal and real-time constraints. A transformation algorithm from interface interaction automata to timed automata model is designed, which can then be further model checked to verify the properties of the proposed IIA. SpaceWire bus protocol is selected as the experiment subject model checked based on the proposed model and methods to verify the feasibility and effectiveness.