Technical reports

Correctness properties of the Viper black model: the second level

Avra Cohn

May 1988, 114 pages

DOI: 10.48456/tr-134

Abstract

Viper [8,9,10,11,22] is a microprocessor designed by J. Cullyer, C. Pygott and J. Kershaw at the Royal Signals and Radar Establishment in Malvern (RSRE), and is now commericially available. Viper is intended for use is safety-critical applications such as aviation and nuclear power plant control. To this end, Viper has a particularly simple design about which it is relatively easy to reason using current techniques and models. The designers at RSRE, who deserve much credit for the promotion of formal methods, intended from the start that Viper be formally verified. This report describes the partially completed correctness proof, in the HOL system, of the Viper ‘block model’ with respect to Viper’s top level functional specification. The (fully completed) correctness proof of the Viper ‘major state’ model has already been reported in [5]. This paper describes the analysis of the block model in some detail (in sections 6 to 9), so is necessarily rather long. A less detailed account is to appear in future [6]. Section 2 is a discussion of the scope and limits of the word ‘verification’, and cautions against careless use of the term. The paper includes a very brief introduction to HOL (section 4), but does not attempt a description or rationalization of Viper’s design. The possible uses of the paper are as follows:

It includes enough detail to support an attempt to repeat the proof in HOL, or possibly in other theorem-proving systems.

It serves as a guide for future analyses of Viper;

It completes the existing Viper documentation;

It covers some general issues in hardware verification;

It illustrates the probelms in managing large HOL proofs.

Full text

PDF (7.0 MB)

BibTeX record

@TechReport{UCAM-CL-TR-134,
  author =	 {Cohn, Avra},
  title = 	 {{Correctness properties of the Viper black model: the
         	   second level}},
  year = 	 1988,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-134.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-134},
  number = 	 {UCAM-CL-TR-134}
}