Formally Linking Verification Systems
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
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
the detection of design errors that lead to users making systematic errors.
The following people are involved with the project:
The project research fall into three main areas:
- The verification of hybrid tools
- The development of a practical hybrid tool (primarily done at Concordia)
- The verification of Interactive Systems.
The key advances that have resulted from the project in these areas are
Below we give overviews of each of the three main areas of the project.
- The development of a hybrid verification tool that provides explicit
support for hierarchical hardware verification (at Concordia University).
- The machine-checked verification of the translation phases of a specification
of such a system.
- The proof of theorems that justify the importing of results from an
automated hardware verification system into an interactive proof system.
- 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.
- 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
This was the core part of the project concerned with the way that we trust
hybrid verification systems. Much of the work forms the core of Haiyan Xiong's
Thesis. HOL code for this work is available.
- 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
The main focus of the EPSRC grant was on the verification aspects above.
However, a consequence of the grant was that we were able to take part in
the development of the MDG-HOL Hybrid verifciation system at Concordia University.
- 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.
- 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.
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
Publications arising from the project
Full Papers in Journals or International Conferences
- 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.
- 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.
- 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
- 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).
- 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
- 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
- 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
- H. Xiong, P. Curzon, S. Tahar and A. Blandford, "Providing a
Formal Linkage between MDG and HOL", submitted for publication,
- 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
- H. Xiong, Providing a Formal Linkage between MDG and HOL based on
a Verified MDG System, PhD Thesis, Middlesex University,
- 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.
- 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
- 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.
- 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.
- 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
- 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.
- 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.
- 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
- 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
- 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.
- 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
- 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.
- 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.
- P. Curzon, "Integrating Source to Source Translations into the
MDG-HOL Hybrid Tool and its Verification", Working Paper, Middlesex
University, September 2001.
HOL code arising from the project
HOL files linked to the project can be obtained from here.
It includes full formal specifications and proof developments including semantics of the
languages, definition of the translator, development of the linkage theorems and the
example proof development. Specifically this is the code of the work described in the paper
"Providing a Formal Linkage between MDG and HOL" which is currently under review.