A formal approach for modeling and verification of bus bridge based on Petri Net and model checking

Embedded systems use many complex bus protocols for data transfer because of the merits of shared resources, low cost of implementation and high performance. Bus bridges are used for conversion and communication among these protocols. This paper describes the formal verification of the Petri Net models of bus bridge using model checking techniques. Typical structure of the bus bridge is introduced and an efficient algorithm is proposed to translate FSM model into Petri Net. The methodology presented addresses the model checking of critical properties of bus bridge including safety, liveness and fairness properties which are expressed in computation tree logics. Finally a general example is given in order to show the validity of the proposed methodology.