The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verification reliability and automation.To solve the above problems,this paper proposes a nonline...The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verification reliability and automation.To solve the above problems,this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan’s refinement rules.First,we use recursive definition technique to characterize the initial specification.The specification is then transformed into GCL(Guarded Command Language)programs using loop invariant derivation and Morgan’s refinement rules.Furthermore,VCG(Verification Condition Generator)is used in the GCL program to generate the verification condition automatically.The Isabelle theorem prover then validates the GCL program’s correctness.Finally,the GCL code generates a C++executable program automatically via the conversion system.The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example.This method addresses the problem that the construction process’s loop invariant is difficult to obtain and the refinement process is insufficiently detailed.At the same time,the method improves verification process automation and reduces the manual verification workload.展开更多
Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyz...Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model- checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain （DTMC） that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications： a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.展开更多
In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs （MDGs） theory i...In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs （MDGs） theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams （ROBDDs） to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae （DF）. Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.展开更多
基金Supported by the National Natural Science Foundation of China(62262031)Science and Technology Key Project of Education Department of Jiangxi Province(GJJ2200302,GJJ210307)the Graduate Innovative Special Fund Projects of Jiangxi Province(YJS2022064)
文摘The traditional program refinement strategy cannot be refined to an executable program,and there are issues such as low verification reliability and automation.To solve the above problems,this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan’s refinement rules.First,we use recursive definition technique to characterize the initial specification.The specification is then transformed into GCL(Guarded Command Language)programs using loop invariant derivation and Morgan’s refinement rules.Furthermore,VCG(Verification Condition Generator)is used in the GCL program to generate the verification condition automatically.The Isabelle theorem prover then validates the GCL program’s correctness.Finally,the GCL code generates a C++executable program automatically via the conversion system.The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example.This method addresses the problem that the construction process’s loop invariant is difficult to obtain and the refinement process is insufficiently detailed.At the same time,the method improves verification process automation and reduces the manual verification workload.
文摘Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model- checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain （DTMC） that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications： a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.
文摘In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs （MDGs） theory in HOL. MDGs generalize Reduced Ordered Binary Decision Diagrams （ROBDDs） to represent and manipulate a subset of first-order logic formulae. The MDGs embedding is based on the logical formulation of an MDG as Directed Formulae （DF）. Then, the MDGs operations are defined and the correctness proof of each operation is provided. The MDG teachability algorithm is then defined as a conversion that uses our MDG theory within HOL. Finally, a set of experimentations over benchmark circuits has been conducted to ensure the applicability and to measure the performance of our approach.
