Formal Verification of SNPP Based on UPPAAL
Rongsheng Dong · Journal of Guangxi Academy of Sciences · 2010
The transaction actions between different banks and the overtime of main bodies in Simple Network Payment Protocol are analyzed.The timed automata models of customer,merchant,banks and overtime timer are established.UPPAAL is used to verify the satisfication of protocol with goods atomicity.The new model,based on the original one,adds overtime timer to receive the overtime informations from other processes and sends out overtime messages after overtime timer of each main bodies are triggered.Then the issue is solved by external arbitration procedure.The new model satisfies money and goods atomicity,and is more suitable than the original for the protocol in realistic environment.