MDG-HOL

Introduction

Research Results

Publications

HOL code

Formally Linking Verification Systems

Introduction

This project, carried out at Middlesex University was concerned with the machine-checked verification of hybrid verification systems where a decision diagram based system is verified in and linked to a theorem prover. A major contribution ot the work concerns formal verification of the way results from a decision diagram system are imported into a theorem prover. Furthermore, we have shown how such results can be combined with verification results about a hardware verification system. We are using as a case study the verification of a linkage between the MDG Hardware verification System and the HOL Theorem Proving System. The verification work has been performed using HOL. Part of the work has involved collaboration with a project at Concordia University on the design and implementation of a practical hybrid verification system (MDG-HOL) . It is tailored for conducting Hierarchical hardware verification.

The project is funded by the EPSRC on a Fast Stream research grant (GR/M45221). The work is in collaboration with Condordia University, Canada and the University of Cambridge, UK.

A case study on a simple hardware design used in the early stages of this project has developed into interesting research in its own right on the detection of design errors that lead to users making systematic errors.

The following people are involved with the project:

• Paul Curzon, now at Queen Mary, University of London (Principle Investigator)
• Haiyan Xiong, Middlesex University, UK
• Ann Blandford, Now at University College London, UK
• Sofiene Tahar, Concordia University, Canada
• Mike Gordon, Cambridge University

Research Results

The project research fall into three main areas:

1. The verification of hybrid tools
2. The development of a practical hybrid tool (primarily done at Concordia) and
3. The verification of Interactive Systems.
   

The key advances that have resulted from the project in these areas are thus:

1. The development of a hybrid verification tool that provides explicit support for hierarchical hardware verification (at Concordia University).
2. The machine-checked verification of the translation phases of a specification of such a system.
3. The proof of theorems that justify the importing of results from an automated hardware verification system into an interactive proof system.
4. A demonstration of how verification results concerning an automated verification tool can be combined with results about the linkage in a hybrid verification system using the combination of hardware verification and usability verification as a case study.
5. The development of a novel approach to the usability verification of interactive systems that supports the detection of design errors that would result in the operators of the system making systematic errors including the development of a novel higher-order logic cognitive model.

Verified Hybrid Verification Systems

Importing Theorems:

We have proved theorems justifying the exporting of results from the MDG verification tools into HOL. These theorems are expressed in a form independent of the semantics of any particular system. They could therefore be applied to other systems with a similar architecture. The specific applications considered were: combinational, sequential verification and property checking.

Verified Translation:

A translator has been verified that translates from a significant (binary decision diagram) subset of MDG-HDL (the hardware description language of MDG) to a TABLE subset of the language and then into a decision diagram language. A deep embedding semantics of a subset of the MDG-HDL subset has been provided. A multi-pass translator for this subset has been formally specified. A correctness theorem for this translator has been proved. This work was all done within the HOL theorem prover and so is machine-checked.

Existential Theorems:

Importing theorems require existential theorems be proved similar to those required to show that a specification is not vacuous. A methodology for proving both kinds of existential theorems has been developed together with supporting HOL tactics to aid in their proof.

Formal Linkage:

The justification theorems and translation correctness theorem have been formally linked using a common formal semantics for the MDG-HDL subset. This in effect means that results proved by the MDG tools in terms of low level data structures can be formally converted to results of the form, in terms of MDG-HDL, imported into HOL.

Case Study:

A small case study was carried out. It demonstrated the verification methodology and how results about low level MDG constructs proved using MDG could be converted to high level results in HOL and then combined with usability verification results proved in HOL.

Source Level Transformation:

The integration of trusted source transformations within the hybrid tool, for example to make the verification more tractable, has been examined. As part of this study, we also compared approaches to verifying translators and writing fully expansive proof based translators in hybrid verification systems. This has resulted in the identification of areas for further research integrating a transformational verification system with the hybrid tool. The Concordia team are keen to develop this further.

Hybrid Tool Development

A Practical Hybrid Tool:

A prototype hybrid tool was developed that demonstrated the feasibility of linking HOL and MDG. The approach used is applicable to other combinations of hardware verification tools. The prototype hybrid tool was reengineered to provide a tool that could be applied to significant examples. This tool included facilities for doing automatic MDG combinational verification and sequential verification within HOL. It also provides a facility for automatically breaking down a verification problem into the verification of its components. This is done using HOL proof.

Case Study:

A study based on an ATM switch fabric was performed. It was shown that verification using the tool was significantly faster than was possible either with MDG or HOL alone.

Parameterised Circuit Verification:

An outline design for integrating parameterised circuit verification automatically with the tool was developed. The ability to do such verification of parameterised circuits is a major area that hybrid systems give advantages over non-hybrid systems. Ongoing work at Concordia is integrating parameterised circuit verification into the hybrid tool.

Comparing Verification Systems:

The project resulted from work comparing interactive proof and automatic verification systems for hardware verification. The ongoing collaboration resulting from this grant led to further publication of this work.

 

Verification of Interactive Systems

In addition to the work directly related to the project objectives, a novel approach to the verification of interactive systems has been developed. This arose from a case study for the hybrid tool. The aim was to show how a hybrid tool might be applied to an application mixing hardware verification with verification of other aspects of a system. However, the case study then raised interesting issues in its own right with respect to the verification of interactive systems. We give an overview of the early results here.

A formal, generic user model:

A generic user model has been developed in higher-order logic. It embodies simple rational behaviour based on user goals and knowledge. It can be instantiated for a range of different interactive devices.

Detecting Systematic User Errors:

The methodology can be used to detect a diverse range of design errors that lead to users making systematic errors. This includes: post completion errors; order errors based on communication goal problems; user errors due to lack of guidance for non-communication goals; user errors due to lack of feedback during computation delays; user errors due to dynamic changes in the interface that are not in response to user input.

Case Studies:

A series of case studies have been performed demonstrating how the absence of such design errors can be demonstrated and how problems in erroneous systems is detected. It was shown that a correctness theorem resulting from this methodology could be formally combined with a traditional formal hardware verification result.

Model Checking:

The feasibility of using model checking has also been investigated and a design for the way user behaviour would be modelled in such a system has been evaluated as a basis for further research on the use of a hybrid verification tool in pure usability verification. This is ongoing work.

Publications arising from the project

Full Papers in Journals or International Conferences

1. S. Kort, S. Tahar and P. Curzon. "Hierarchical Formal Verification Using a Hybrid Tool". Int. J. on Software Tools for Technology Transfer 4 pp1-10, Springer 2002.
2. H. Xiong, P. Curzon, S. Tahar and A. Blandford, "Formally Linking MDG and HOL based on a Verified MDG System", Proceedings of the Third International Conference on Integrated Formal Methods, Edited by M. Butler, L. Petre and K. Sere, Lecture Notes in Computer Science 2335, pp205-224, Turku, Finland, May 2002.
   
3. S. Kort, S. Tahar and P. Curzon. "Hierarchical Formal Verification Using an MDG-HOL Hybrid Tool", Correct Hardware Design and Verification Methods, Proc.11th IFIP WG 10.5 Advanced Research Working Conf, CHARME 2001, Eds. T. Margaria and T. Melham, LNCS 2144, pp 244-258, Springer, September 2001. ps file
4. P. Curzon and A. Blandford, "Detecting Multiple Classes of User Errors", Proceedings of the 8th IFIP Working Conference on Engineering for Human-Computer Interaction (EHCI'01), LNCS, May 2001 Springer-Verlag. In press. (Also published in the Conference pre-proceedings).
5. V.K. Pisini, S. Tahar, P. Curzon, O. Aït-Mohamed and X. Song: "Formal Hardware Verification by Integrating HOL and MDG". Proceedings of the ACM 10th Great Lakes Symposium on VLSI, Chicago, Illinois, USA, March 2000, ACM Publications, pp. 23-28. Available from the ACM Digital Library
6. P. Curzon and S. Tahar, "Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric". Nordic Journal of Computing, pp372-402, 6(4) Winter 1999. ps file
7. H. Xiong, P. Curzon and S. Tahar, "Importing MDG Verification Results into HOL". Theorem Proving in Higher Order Logics: 12th Int. Conf, LNCS 1690, pp 293-310, Springer 1999. ps file

Other Publications

1. H. Xiong, P. Curzon, S. Tahar and A. Blandford, "Providing a Formal Linkage between MDG and HOL", submitted for publication, 2003.
2. Haiyan Xiong, Paul Curzon, Sofiene Tahar and Ann Blandford (2003) Providing a formal linkage between the MDG verification system and HOL proof system. Middlesex University Interaction Design Centre Technical Report: IDC-TR-2003-006. pdf (29 pages)
3. H. Xiong, Providing a Formal Linkage between MDG and HOL based on a Verified MDG System, PhD Thesis, Middlesex University, 2002.
4. P. Curzon and S. Tahar, "Automating the Verification of Parameterized Hardware using a Hybrid Tool", Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001, pp. 257-260. ps file
5. H. Xiong, P. Curzon, S. Tahar and A. Blandford, "Proving Existential Theorems when Importing Results from MDG to HOL", TPHOLs 2001: Supplementary Proc., ed. by R.J.Bolton and P.B. Jackson, U. of Edinburgh, Informatics Research Report, ED-INF-RR-0046, pp 384-399, 2001. ps file
6. P. Curzon and A. Blandford, "A User Model for Avoiding Design Induced Errors in Soft-Key Interactive Systems", TPHOLs 2001: Supplementary Proceedings, ed by R.J.Bolton and P.B. Jackson, U. of Edinburgh, Informatics Research Report, ED-INF-RR-0046, pp 33-48, 2001.
7. P. Curzon and A. Blandford, "Reasoning about Order Errors in Interaction", The Supplementary Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, edited by M. Aagaard, J. Harrison and T. Schubert, Oregon Graduate Institute, Technical Report CSE 00-009, pp 33-48, August 2000, Portland U.S.
8. H. Xiong, P. Curzon, S. Tahar and A. Blandford, "Embedding and Verification of an MDG-HDL Compiler in HOL", The Supplementary Proc. of the 13th International Conference on Theorem Proving in Higher Order Logics, edited by M. Aagaard, J. Harrison and T. Schubert, Oregon Graduate Institute, Technical Report CSE 00-009, pp 237-248, August 2000, Portland U.S. ps file
9. P. Curzon and A. Blandford, "Using a Verification System to Reason About Post-Completion Errors". Participants Proc. of DSV-IS 2000: 7th Int.Workshop on Design, Specification and Verification of Interactive Systems, at the 22nd Int. Conf. on Software Engineering, ed by P. Palanque and F. Paternò, pp 292-308, 2000.
10. S. Kort, V.K. Pisini, S. Tahar, O. Ait-Mohamed, P. Curzon and X. Song: "Un outil hybride pour la vérification formelle de circuits"; Proc. 68th ACFAS Symposium (ACFAS'00), May 2000.
11. M. Hasan, S. Tahar, and P. Curzon "Impact of Design Changes on Verification Using MDGs" Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000, pp. 173-178. pdf file
12. S. Kort, S. Tahar, P. Curzon, X. Song: "HOL-MDG: A Hybrid Tool for Formal Verification"; Proc. 2000 Micronet Workshop, Ottawa, Canada, April 2000, pp. 131-132. pdf file
13. P. Curzon and A. Blandford,. "Reasoning about Order Errors and Interaction", Proc. C@MDX'00, Research Student's Conference, Middlesex University School of Computing Science, March 2000.
14. V.K. Pisini, S. Tahar, O. Aït-Mohamed, P. Curzon, and X. Song. "An Approach to Link HOL and MDG for Hardware Verification". Proc. of the 1999 Micronet Workshop, Ottawa, Canada, April 1999, pp. 156-157. ps file
15. H. Xiong, P. Curzon and A. Blandford. "Combining Verification Systems in a Trusted Way to Reap the Benefits of Both". 6th Workshop on Automated Reasoning-Bridging the Gap between Theory and Practice. pp71-73, April 1999.
16. H. Xiong, P. Curzon, S. Tahar and A. Blandford. "Verification of a Translator for MDG's Library in HOL". 15th British Colloquium for Theoretical Computer Science. April 1999.
17. P. Curzon, "Integrating Source to Source Translations into the MDG-HOL Hybrid Tool and its Verification", Working Paper, Middlesex University, September 2001.