Dan Zhou and Paul E. Black, Translating HOL to Specifications for the Model Checker SMV, TPHOLs 2001, supplemental proceedings, pages 400-415, Edinburgh, Scotland (September 2001).

Abstract:

    HOL and SMV have two radically different formal specification languages. Each is good at describing different aspects of systems and have very different analysis tools. We want to integrate them to make full use of their respective capabilities. One step towards this integration is automatically translating specifications written in HOL into SMV. We argue for the need of such an integration and translation for specification-based testing. We look at the differences between HOL and SMV and specify mechanical translation methods which are appropriate for modeling and testing secure operating systems.

Get the paper in Postscript (177k) or PDF (198k).

This page's URL is /~black/Papers/hol2smvTPHOL2001.html

Updated Mon Apr 7 18:21:43 2003

Go to Black's papers or NIST home page.