Research Of Embedded Software Formalization Modeling And Verification Method Based On STM

With the rapid development and wide application of computer technology, software systems are playing a more and more important role. Once software systems fail, the consequences will be immeasurable. So facing the increasing complexity of software, how to effectively guarantee the realiability of software has become a huge challenge. The software formal verification technology based on model has become one of the primary means to guarantee software reliability.In view of the deficiency of the expression ability of modeling language and state space explosion in model checking field, this work studies from formal model and compression methods, symbolic coding and verification.Firstly, for the defects of traditional state transition matrix (STM), a new modeling method named hierarchical timed state transition matrix (HTSTM) is proposed. This method models software systems hierarchically to ease state space explosion problem caused by the increase of states and events. In order to solve the problem that traditional STM can not express time semanteme, the new method introduces time events into the model as actions to tigger the system. These improvements make this method closer to the actual software modeling requirements. Based on bounded model checking (BMC) we present a symbolic encoding method and property design method. Thereby the complete software formal modeling and verification process is formed. The experiment results based on complex software of engineering background prove the feasibility and effectiveness of the method.Secondly, to solve complex software model and state space explosion problem, we present a state compression algorithm of timed automaton. This algorithm compresses the states of automaton based on the symbolization of timed conditions. We examine the effect of the compression method through using SMT and UPPAAL model validation tools to test the time and performance parameters of uncompressed model and compressed model. As we can see from the experimental data, by the compression algorithm the validation performances are improved effectively and the state space explosion problem is solved for a certain extent. In addition, the states compression algorithm the paper presents has used in practical application of changhong smart TV test project, and achieved good results.