Abstract: Model-based techniques for system designs and analysis can effectively satisfy high reliability requirements of modern embedded software system. In this paper,an improved version of prototype T-CI3ES1)was designed and imple- mented based on On-thcfly verification mechanism Specifically, a graphic modeling environment was provided by in- tegrating Topcased and JFLAP into T-CI3ESD framework, and pre-translation transformation algorithms were also de- signed. The data structures of state space were redesigned and several kinds of consistency verification algorithm based on On-thcfly method were designed and implemented, which include analysis and verification frameworks for functional and non-functional system behaviors. Moreover, one example was shown by using the improved version of T-CBESD.

Key words: Eembedded software design, UML interactive overview diagram, Interface automata, On-the-fly verification algorithm, Formal verification tool