利用即时验证方法的T-CBESD工具扩展设计与实现

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-CBESD (Tool for Component-Based Embedded Software Designs) has been designed and implemented based on On-the-fly verification mechanism. Specifically, a graphic modeling environment is provided by integrating Topcased and JFLAP into T-CBESD framework, and model-transformation algorithms are also designed, including pre-translation from UML interactive overview diagrams to a set of message event sequences, from JFLAP automaton models to different kinds of interface automata, etc. Meanwhile, the data structures of state space are redesigned and several kinds of consistency verification algorithm based on On-the-fly method are designed and implemented, which include analysis and verification frameworks for functional and non-functional system behaviors. Moreover, two examples are shown by using the improved version of T-CBESD.