Font Size: a A A

The Research And Implementation Of Algorithms For Model-Checking Tool FPTAT For Real-Time Systems

Posted on:2006-10-02Degree:MasterType:Thesis
Country:ChinaCandidate:Y B XuFull Text:PDF
GTID:2168360152987466Subject:Computer software and theory
Abstract/Summary:PDF Full Text Request
Model-checking is one of the most successful automatic verification techniques in the past two decades, which has been used in the analysis and verification of finite-state systems such as communication protocols and sequential circuit designs. Safety of real-time systems has acquired an extensive attention in real-time application fields. And the method of model-checking conduces to advancing safety of real-time systems, because it is helpful to find some errors and bugs effectively during the process of system design in real-time systems.At present, there exist many fundamental researches on the theories and methods of model-checking for real-time systems. Accordingly, some algorithms in model-checking and verification tools have been implemented, most of which are based on discrete semantic models or continuous semantic models.Finite precision timed automaton (FPTA), introduced in this thesis, based on timed automata with continuous semantics, is a simplified semantic model, i.e., finite precision semantic model. Combining the respective virtues of discrete semantic models and continuous semantic models, finite precision semantic models can represent asynchronous systems. Besides, the relevant model-checking algorithm is relatively simple, due to the integer valuation of clock variables in the model. Based on FPTA theory, we implement a model-checking tool, named FPTAT, used for reachability analysis and verification of real-time systems. And a kind of symbolic method for model-checking is applied to the tool FPTAT. From experiment results, it can be concluded that the performance of the tool is good.The work mainly includes:1. Having designed the model-checking algorithm for real-time systems based on finite precision timed automata theory and symbolic methods, and implemented a model-checking tool FPTAT for real-time systems, which demonstrates good efficiency of the algorithm with some examples.2. Having implemented a kind of symbolic method for model-checking, i.e., using the data structure SDS ( Series of Delay Sequences ) to represent state sets in state space symbolically. Based on this, a two-layer hash index structure is presented to organize the state space.3. Having introduced the active clock theory into the process of model-checking based on FPTA theory. And it is helpful reducing the memory of state effectively, as a result, improving the efficiency of model-checking.
Keywords/Search Tags:model-checking tools, real-time systems, timed automata, finite precision, symbolic methods
PDF Full Text Request
Related items