Abstract
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.
基金项目
Natural Science Foundation of Jiangsu Province in China(BK20191475)
fifth phase of"333 Project"scientific research funding project of Jiangsu Province in China(BRA2020306)
Qing Lan Project of Jiangsu Province in China(2019)
NETL
NSTL
万方数据