Automatic verification of reduction techniques in Higher Order Logic

In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG–HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one is the reduction using SAT–MDG of an Island Tunnel Controller and the second one is the MDG–HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage.     

Multiway Decision Graphs for Automated Hardware Verification

Traditional ROBDD-based methods of automated verification suffer from the drawback that they require a binary representation of the circuit. To overcome this limitation we propose a broader class of decision graphs, called Multiway Decision Graphs (MDGs), of which ROBDDs are a special case. With MDGs, a data value is represented by a single variable of abstract type, rather than by 32 or 64 boolean variables, and a data operation is represented by an uninterpreted function symbol. MDGs are thus much more compact than ROBDDs, and this greatly increases the range of circuits that can be verified. We give algorithms for MDG manipulation, and for implicit state enumeration using MDGs. We have implemented an MDG package and provide experimental results.     

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

NuMDG: A New Tool for Multiway Decision Graphs Construction

Multiway Decision Graphs(MDGs) are a canonical representation of a subset of many-sorted first-order logic. This subset generalizes the logic of equality with abstract types and uninterpreted function symbols.The distinction between abstract and concrete sorts mirrors the hardware distinction between data path and control.Here we consider ways to improve MDGs construction.Efficiency is achieved through the use of the Generalized-If-Then-Else(GITE) commonly operator in Binary Decision Diagram packages.Consequently,we review the main algorithms used for MDGs verification techniques.In particular,Relational Product and Pruning by Subsumption are algorithms defined uniformly through this single GITE operator which will lead to a more efficient implementation.Moreover,we provide their correctness proof.This work can be viewed as a way to accommodate the ROBBD algorithms to the realm of abstract sorts and uninterpreted functions.The new tool,called NuMDG,accepts an extended SMV language,supporting abstract data sorts.Finally,we present experimental results demonstrating the efficiency of the NuMDG tool and evaluating its performance using a set of benchmarks from the SMV package.     

Mechanizing some advanced refinement concepts

We describe how the HOL theorem prover can be used to check and apply rules of program refinement. The rules are formulated in the refinement calculus, which is a theory of correctness preserving program transformations. We embed a general command notation with a predicate transformer semantics in the logic of the HOL system. Using this embedding, we express and prove rules for data refinement and superposition refinement of initialized loops. Applications of these proof rules to actual program refinements are checked using the HOL system, with the HOL system generating these conditions. We also indicate how the HOL system is used to prove the verification conditions. Thus, the HOL system can provide a complete mechanized environment for proving program refinements.     

An embedding of Timed Transition Systems in HOL

The theory of Timed Transition Systems developed by Henzinger, Manna, and Pnueli provides a formal framework for specifying and reasoning about real-time systems. In this paper, we report on some preliminary investigations into the mechanization of this theory using the HOL theorem prover.We review the main ideas of the theory and describe how it has been formally embedded in HOL. A graphical notation of timed transition diagrams and a real-time temporal logic for requirements have also been embedded in HOL using the embedding of timed transition systems. The proof rules proposed by Henzinger et al have been verified formally and we illustrate their use, as well as some problems we have encountered, by reference to a small example. More work is required on interfaces and proof methods to have a generally usable system.     

Self-Formalisation of Higher-Order Logic

We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem prover. Our work extends Harrison’s verification of the inference system without definitions. Soundness of the logic extends to soundness of a theorem prover, because we also show that a synthesised implementation of the kernel in CakeML refines the inference system. Apart from adding support for definitions and synthesising an implementation, we improve on Harrison’s work by making our model of HOL parametric on the universe of sets, and we prove soundness for an improved principle of constant specification in the hope of encouraging its adoption. Our semantics supports defined constants directly via a context, and we find this approach cleaner than our previous work formalising Wiedijk’s Stateless HOL.     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

Scheduling multicast traffic in input-buffered ATM switch

Performance of an input-buffered ATM switch is limited by the head-of-line (HOL) blocking problem. HOL blocking is even more pronounced in multicast switch where cells compete for multiple outputs simultaneously. Previous studies in input-buffered unicast switch have shown that HOL blocking can only be eliminated by using per-output queuing and sophisticated scheduling methods, such as the maximal weight matching (MWM) or the parallel iterative matching (PIM) methods. The MWM or PIM types of scheduling algorithm cannot be applied to multicast switch because of the high computation complexity. In this paper, we present a reservation based scheduling algorithm, which employs per-VC queuing for multicast connections and per-output queuing for unicast connections. Instead of the input ports sending a huge amount of state information to the output ports for processing, we circulate reservation vectors amongst the input ports. Each input port will then make reservation based on its local state and the availability of the output ports. The scheduling is done on a frame by frame basis. While the input ports are transmitting cells according to the schedule of the current frame, the next frame schedule is computed. Simulations reveal that our method substantially outperforms the methods that employ FIFO queuing discipline.     

Analysis of multiple sources delayed releasing SVCC based data communications over ATM

IP over ATM, Lan Emulation and other technologies of data communications over ATM use ATM switched VCC (SVCC) as the underlying transferring channel. This article analyzes a delayed releasing SVCC based method under multiple sources condition. A single-queue method and a HOL multi-priority queue method are explored. Both theoretical analysis and simulation results are given in this article. It is showed that multi-priority queue method requires less releasing timer T and hence the SVCC usage is made more efficient. A two-queue scheme is proposed as an application of HOL scheduling delayed releasing SVCC scheme. An optimum design target with multiple sources is defined at the end of this article and optimum design method under some simple cases are also included.     

Hierarchical formal verification using a hybrid tool

We describe a hybrid formal hardware verification tool that links the HOL interactive proof system and the MDG automated hardware verification tool. It supports a hierarchical verification approach that mirrors the hierarchical structure of designs. We obtain the advantages of both verification paradigms. We illustrate its use by considering a component of a communications chip. Verification with the hybrid tool is significantly faster and more tractable than using either tool alone. Published online: 19 November 2002     

The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective)

We show how to mechanise equational proofs about higher-order languages by using the primitive proof principles of first-order abstract syntax over one-sorted variable names. We illustrate the method here by proving (in Isabelle/HOL) a technical property which makes the method widely applicable for the λ-calculus: the residual theory of β is renaming-free up-to an initiality condition akin to the so-called Barendregt Variable Convention. We use our results to give a new diagram-based proof of the development part of the strong finite development property for the λ-calculus. The proof has the same equational implications (e.g., confluence) as the proof of the full property but without the need to prove SN. We account for two other uses of the proof method, as presented elsewhere. One has been mechanised in full in Isabelle/HOL.     

Information assurance the West Point way

At the US Military Academy at West Point, New York, we approach the topic of protecting and defending information systems as a matter of national security. The time has long passed where we could consider cyberattacks as merely a nuisance; the threat from a cyberattack is very real. Our national information infrastructure is not just essential to the USA economy; it is a life-critical system. Presidential Decision Directive 63 (which called for a national effort to assure vulnerable and interconnected infrastructure security, such as telecommunications, finance, energy, transportation, and essential government services) officially recognizes this, and numerous reports have validated it. As military academy educators, our duty is to provide an education that empowers our graduates with the skills needed to protect the many critical information systems that the military uses.     

连续不确定决策系统及其扩展Rough集分析

连续不确定决策表可视为一种多值表元决策表。利用Fuzzy集理论可将多值表元决策表转换为带有隶属度的单一表元决策表;并在此基础上,给出了扩展信息表和决策表的定义,提出了对多值表元决策表中决策概念下近似及边界的计算方法,为利用规则推导算法产生知识提供了确定的输入。     

A reversible data hiding scheme based on the Sudoku technique

Data hiding, also known as information hiding, plays an important role in information security for various purposes. Reversible data hiding is a technique that allows distortion-free recovery of both the cover image and the secret information. In this paper, we propose a new, reversible data hiding scheme that is based on the Sudoku technique and can achieve higher embedding capacity. The proposed scheme allows embedding more secret bits into a pair of pixels while guaranteeing the good quality of the stego-image. The experimental results showed that the proposed scheme obtained higher embedding capacity than some other previous schemes. In addition, our proposed scheme maintained the good visual quality of the stego-image (i.e., PSNR > 46 dB), which outperforms some existing schemes.     

A verification approach to applied system security

We present a method for the security analysis of realistic models over off-the-shelf systems and their configuration by formal, machine-checked proofs. The presentation follows a large case study based on a formal security analysis of a CVS-Server architecture.The analysis is based on an abstract architecture (enforcing a role-based access control), which is refined to an implementation architecture (based on the usual discretionary access control provided by the POSIX environment). Both architectures serve as a skeleton to formulate access control and confidentiality properties.Both the abstract and the implementation architecture are specified in the language Z. Based on a logical embedding of Z into Isabelle/HOL, we provide formal, machine-checked proofs for consistency properties of the specification, for the correctness of the refinement, and for security properties.     

Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL

Real-time systems usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism, which makes their performance analysis quite complex. Thus, traditional techniques, such as simulation, or the state-based formal methods usually fail to produce reasonable results. In this paper, we propose to use higher-order-logic (HOL) theorem proving for the performance analysis of real-time systems. The idea is to formalize the real-time system as a logical conjunction of HOL predicates, whereas each one of these predicates define an autonomous component or process of the given real-time system. The random or unpredictable behavior found in these components is modeled as random variables. This formal specification can then be used in a HOL theorem prover to reason about both functional and performance related properties of the given real-time system. In order to illustrate the practical effectiveness of our approach, we present the analysis of the Stop-and-Wait protocol, which is a classical example of real-time systems. The functional correctness of the protocol is verified by proving that the protocol ensures reliable data transfers. Whereas, the average message delay relation is verified in HOL for the sake of performance analysis. The paper includes the protocol’s formalization details along with the HOL proof sketches for the major theorems.     

Certified Quantum Computation in Isabelle/HOL

In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch’s algorithm, the Deutsch–Jozsa algorithm and the quantum Prisoner’s Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.