检索规则说明:AND代表“并且”;OR代表“或者”;NOT代表“不包含”;(注意必须大写,运算符两边需空一格)
检 索 范 例 :范例一: (K=图书馆学 OR K=情报学) AND A=范并思 范例二:J=计算机应用与软件 AND (U=C++ OR U=Basic) NOT M=Visual
作 者:Zhenjiang Qian Gaofei Sun Xiaoshuang Xing Gaurav Dhiman
机构地区:[1]School of Computer Science and Engineering,Changshu Institute of Technology,Suzhou,215500,China [2]University Centre for Research and Development,Department of Computer Science and Engineering,Chandigarh University,Mohali,140413,India [3]Department of Computer Science and Engineering,Graphic Era Deemed to be University,Dehradun,248002,India
出 处:《Digital Communications and Networks》2024年第2期304-314,共11页数字通信与网络(英文版)
基 金:supported in part by the Natural Science Foundation of Jiangsu Province in China under grant No.BK20191475;the fifth phase of“333 Project”scientific research funding project of Jiangsu Province in China under grant No.BRA2020306;the Qing Lan Project of Jiangsu Province in China under grant No.2019.
摘 要:In traditional digital twin communication system testing,we can apply test cases as completely as possible in order to ensure the correctness of the system implementation,and even then,there is no guarantee that the digital twin communication system implementation is completely correct.Formal verification is currently recognized as a method to ensure the correctness of software system for communication in digital twins because it uses rigorous mathematical methods to verify the correctness of systems for communication in digital twins and can effectively help system designers determine whether the system is designed and implemented correctly.In this paper,we use the interactive theorem proving tool Isabelle/HOL to construct the formal model of the X86 architecture,and to model the related assembly instructions.The verification result shows that the system states obtained after the operations of relevant assembly instructions is consistent with the expected states,indicating that the system meets the design expectations.
关 键 词:Theorem proving Isabelle/HOL Formal verification System modeling Correctness verification
分 类 号:TN91[电子电信—通信与信息系统]
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在载入数据...
正在链接到云南高校图书馆文献保障联盟下载...
云南高校图书馆联盟文献共享服务平台 版权所有©
您的IP:216.73.216.116