Formal modeling and verification of credit derivative products

Credit derivative products offer great promise in terms of capability and flexibility in separating and transferring the credit risk of the underlying loan, but the properties of the operation process are particularly hard to evaluate. This paper presents a formal methodology of modeling and verification about credit derivative based on extended Petri net and SMV. By translating the extended Petri net model into specification language of the SMV Model, properties of Credit derivative could be completely verified using symbolic model checking technique. The methodology proposed addresses the model checking of critical properties of credit derivative including safety, liveness and fairness properties which are expressed in computation tree logics. As a confirmation of its validity, the methodology described in this paper has been successfully applied to modeling and formal verification of Total Return Swap.