Currently, Transaction Level Modeling (TLM) is being used in the industry to solve a variety of practical problems during the design and deployment of electronic systems. TLM and SystemC gain popularity partly due to their simulation capabilities. However, formal models associated to SystemC designs and TLM descriptions are less developed. This paper describes how to translate SystemC modules defined at transactional level to formal Petri Net models. These models offer help in understanding the behaviour of third party modules used in component-based system. This paper focuses mainly on the translation of blocking and non-blocking Interface Method Calls which are the basis of TLM.