Practical Research On Formal Verification Techniques Based On ATL

This paper investigates the applications of formal modeling and verification techniques based on the logical language of ATL(Alternating-time Temporal Logic),in the field of fair exchange protocols and micro-grid power management systems.This paper has two strands. The first one is for the formal modeling and verification for the contract signing protocol with ATL and the implementation tool of MOCHA, and verifies that whether it satisfies the fairness, timeliness, abuse-freeness specifications. With MOCHA, it is found that the contract signing protocol does not meet the fairness, timeliness and abuse-freeness, leading to potential design problems.The second strand lies in formal modeling and analyze for the complex micro-grid power management system with the extended language of rPATL based on ATL. By the model of PRISM-games, the execution with probability of the complex system is simulated, and the provided electricity and fuel cost within a certain time of every distributed power supply is calculated efficiently. The model shows its strength in conciseness and effectiveness by experimental results.The significance of this paper is as follows. Firstly, the application of specification and verification techniques based on ATL for the contract signing protocol is proposed and several important properties have been verified by a software tool that can help improve the protocol design. Secondly, the application of the extended language of rPATL based on ATL has been introduced to the new domain of the emerging micro-grid network, and the formal modeling and simulation to calculate the provided electricity and fuel cost within a certain time of every distributed power supply is studied and automatically simulated, which carries some practical significance for the actual deployment of the micro-grid network.In this paper, the system modeling is based on the game-like model, which is a very natural and easy way for describing open systems with interacting components.Additionally, the model in this paper is a highly abstract one, which thus is able to analyze and verify the complex system efficiently and effectively, and also can be very flexible to be extended into other areas and application domains.