Formal Method Integrating B Method And Time Petri Nets

Nowadays people become much more strict with software and its quality, they not only give high standard with the software which make the software much more sophisticated and also much personal to users, but also they want that the software do not crash while they are using them. In the past people depend on excellent software engineer to make a safe design, but now they use formal techniques to develop software that needs high safety. Now what people want to do is to develop as steps that the formal method or formal language tells them.However formal techniques are based on single foundation, they either can describe data structure or data abstraction, or they can describe the operation schema of the software. With the researchers' deep studying, they found that these formal techniques have naturally their own shortcomings. So people become interested in formal method and its integration, successful example like CSP and B Method, CSP and Z Language.In this paper, we want to introduce TB Nets which integrates TPN and B Method. TB Nets is high level Petri Nets. Just as the same as other high level Petri Nets, TB Nets makes the B Method as underlying formal model with TPN as its upper model. So with B Method, we can define some data structure and function defining in TB Nets, and with the TPN, we have ability to describe real-time systems or concurrency systems. In this paper we also want to have some lights in TB Nets's properties, firstly we want to analyze the reachability of TB Nets, reachability is an important tool to analyze the Petri Nets, so we would like to have a look at this problem. Besides we also want to define the liveness and boundedness of TB Nets, these problems have very close relation with reachability. The last problem that we want to have a look at is time constraints. As the TB Nets have the ability to describe real-time systems, so it is also necessary to discuss the problem of time constraints in order to make sure the requirement about time is satisfied.Generally speaking, TB Nets have a large usage than TPN and B Method, for it is integrated with the two methods and it has advantage of the two methods.