通信学报2025，Vol.46Issue(3)：13-27,15.DOI:10.11959/j.issn.1000-436x.2025038
基于时间自动机的数据流通控制建模及验证
Modeling and verification of data circulation control based on timed automata
摘要
Abstract
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 pro-posed 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(en-compassing data brokers),and data supervisors.Subsequently,the security requirements and circulation control proper-ties 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 attri-butes.The proposed method can effectively validate the feasibility,correctness,and security of data circulation control mechanisms.关键词
数据要素流通/访问控制/时间自动机/延伸控制/形式化方法验证Key words
data elements circulation/access control/timed automata/extension control/formal method verification分类
信息技术与安全科学引用本文复制引用
李恒,李凤华,梁琬珩,郭云川,张玲翠,周紫妍..基于时间自动机的数据流通控制建模及验证[J].通信学报,2025,46(3):13-27,15.基金项目
国家重点研发计划基金资助项目(No.2023YFB3106505) （No.2023YFB3106505）
国家自然科学基金资助项目(No.U24A20240,No.62441226)The National Key Research and Development Program of China(No.2023YFB3106505),The National Natural Science Foundation of China(No.U24A20240,No.62441226) （No.U24A20240,No.62441226）
