Modeling and verification of data circulation control based on timed automata

To address the challenges of verifying the feasibility, correctness, and security of cross-domain data circulation control policies in their generation, transmission, and execution, a formal modeling and verification method was proposed based on timed automata and computation tree logic (CTL). Firstly, the formal models were established for the data circulation control process and key entities in data transaction scene, including data providers, data consumers (encompassing data brokers), and data supervisors. Subsequently, the security requirements and circulation control properties were formalized during data transactions using CTL specifications. Finally, the aforementioned timed automaton model was simulated, with formal verification and analysis performed on its behavioral properties and structural attributes. The proposed method can effectively validate the feasibility, correctness, and security of data circulation control mechanisms.