Xiong, Haiyan, Curzon, Paul, Tahar, Sofiène and Blandford, Ann
(2007)
*Providing a formal linkage between MDG and HOL.*
Formal Methods in System Design, 30
(2).
pp. 83-116.
ISSN 0925-9856

Preview |
Text (application/pdf)
304kBFMSD-2007.pdf - Accepted Version |

Official URL: http://dx.doi.org/10.1007/s10703-006-0017-y

## Abstract

We describe an approach for formally verifying the linkage between a symbolic state enumeration system and a theorem proving system. This involves the following three stages of proof. Firstly we prove theorems about the correctness of the translation part of the symbolic state system. It interfaces between low level decision diagrams and high level description languages. We ensure that the semantics of a program is preserved in those of its translated form. Secondly we prove linkage theorems: theorems that justify introducing a result from a state enumeration system into a proof system. Finally we combine the translator correctness and linkage theorems. The resulting new linkage theorems convert results to a high level language from the low level decision diagrams that the result was actually proved about in the state enumeration system. They justify importing low-level external verification results into a theorem prover. We use a linkage between the HOL system and a simplified version of the MDG system to illustrate the ideas and consider a small example that integrates two applications from MDG and HOL to illustrate the linkage theorems.

Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering |
---|---|

Item Type: | Article |

Refereed: | Yes |

Authors: | Xiong, Haiyan and Curzon, Paul and Tahar, Sofiène and Blandford, Ann |

Journal or Publication: | Formal Methods in System Design |

Date: | 2007 |

Digital Object Identifier (DOI): | 10.1007/s10703-006-0017-y |

Keywords: | design; formal hardware verification; hybrid verification systems; mechanical theorem proving; usability verification; system correctness; |

ID Code: | 977375 |

Deposited By: | Danielle Dennie |

Deposited On: | 14 Jun 2013 15:16 |

Last Modified: | 18 Jan 2018 17:44 |

## References:

1Mark D. Aagaard , Robert B. Jones , Roope Kaivola , Katherine R. Kohatsu , Carl-Johan H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings of the 37th conference on Design automation, p.201-206, June 05-09, 2000, Los Angeles, California, United States [doi>10.1145/337292.337388]

2

Andrew Adams , Martin Dunstan , Hanne Gottliebsen , Tom Kelsey , Ursula Martin , Sam Owre, Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.27-42, September 03-06, 2001

3

3. Amjad H (2003) Programming a symbolic model checker in a fully expansive theorem prover. In: Basin D, Wolff B (eds) Theorem proving in higher order logics, vol. 2758 of Lecture Notes in Computer Science, Springer-Verlag, pp. 171-187.

4

David A. Basin , Stefan Friedrich , Marek Gawkowski, Verified Bytecode Model Checkers, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, p.47-66, August 20-23, 2002

5

5. Bensalem S, Ganesh V, Lakhnech Y, Munoz C, Owre S, Rueß H, Rushby J, Rusu V, Saïdi H, Shankar N, Singerman E, Tiwari A (June 2000) An overview of SAL. In: Holloway CM (ed) Fifth NASA Langley formal methods workshop, Hampton, Virginia, USA, NASA Langley Research Center, pp. 187-196.

6

Richard J. Boulton , Andrew Gordon , Michael J. C. Gordon , John Harrison , John Herbert , John Van Tassel, Experience with Embedding Hardware Description Languages in HOL, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, p.129-156, June 22-24, 1992

7

Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]

8

Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]

9

9. Buchberger B (2004) Towards the automated synthesis of a Gröbner bases algorithm. RACSAM 98(1-2):65-75.

10

10. Butterworth R, Blandford AE, Duke D (2000) Demonstrating the cognitive plausibility of interactive systems. Formal Asp Comput 12:237-259.

11

11. Byrne M, Bovair S (1997) A working memory model of a common procedural error. Cogn Sci 21(1):31-61.

12

12. Camilleri A, Gordon M, Melham T (September 1986) Hardware verification using Higher-order logic. In: Borrione D (ed) From HDL descriptions to guaranteed correct circuit designs: Proceedings of the IFIP WG 10.2 Working Conference, Grenoble, France, pp. 43-67.

13

Laurian M. Chirica , David F. Martin, Toward compiler implementation correctness proofs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.185-214, April 1986 [doi>10.1145/5397.30847]

14

Ching-Tsun Chou , Doron Peled, Formal Verification of a Partial-Order Reduction Technique for Model Checking, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.241-257, March 27-29, 1996

15

F. Corella , Z. Zhou , X. Song , M. Langevin , E. Cerny, Multiway Decision Graphs for Automated Hardware Verification, Formal Methods in System Design, v.10 n.1, p.7-46, February 1997 [doi>10.1023/A:1008663530211]

16

16. Crow J, Owre S, Rushby J, Shankar N, Srivas M (1999) A tutorial introduction to PVS. http://www.dcs.gla.ac.uk/prosper/papers.html

17

Editors:, TPHOLs 2000: Supplemental Proceedings, Oregon Graduate Institute School of Science & Engineering, 2000

18

18. Curzon P, Blandford A (June 2000) Using a verification system to reason about post-completion errors. In: Palanque P, Paternó F (eds) Participants Proceedings of DSV-IS 2000: 7th International Workshop on Design, Specification and Verification of Interactive Systems, at the 22nd International Conference on Software Engineering, Limerick, Ireland, Kluwer, pp. 293-308.

19

Paul Curzon , Ann Blandford, Detecting Multiple Classes of User Errors, Proceedings of the 8th IFIP International Conference on Engineering for Human-Computer Interaction, p.57-72, May 11-13, 2001

20

20. Curzon P, Ruksenas R, Blandford A. Formal verification in human error modelling. Submitted for publication.

21

21. Curzon P, Tahar S, Aït-Mohamed O (1998) Verification of the MDG components library in HOL. In: Grundy J, Newey M (eds) Theorem proving in higher-order logics: Emerging trends, Department of Computer Science, The Australian National University, pp. 31-46.

22

Louise A. Dennis , Graham Collins , Michael Norrish , Richard J. Boulton , Konrad Slind , Graham Robinson , Michael J. C. Gordon , Thomas F. Melham, The PROSPER Toolkit, Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems: Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, p.78-92, March 25-April 02, 2000

23

23. Gordon MJ, Milner R, Wadsworth CP (1979) Edinburgh LCF: A mechanised logic of computation, vol. 78 of Lecture Notes in Computer Science, Springer-Verlag.

24

Michael J. C. Gordon, Reachability Programming in HOL98 Using BDDs, Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, p.179-196, August 14-18, 2000

25

M. J. C. Gordon , T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic, Cambridge University Press, New York, NY, 1993

26

26. Grumberg O, Katz S (March 1999) Veritech: Translating among specification and verification tools design principles, http://www.cs.technion.ac.il/labs/ssdl/research/veritech

27

J. Harrison , L. Théry, A Skeptic’s Approach to Combining HOL and Maple, Journal of Automated Reasoning, v.21 n.3, p.279-294, December 1998 [doi>10.1023/A:1006023127567]

28

Scott Hazelhurst , Carl-Johan H. Seger, Symbolic Trajectory Evaluation, Formal Hardware Verification - Methods and Systems in Comparison, p.3-78, January 1997

29

André Heck, Introduction to Maple, Springer-Verlag New York, Inc., New York, NY, 1993

30

30. Hurd J (April 1999) Integrating GANDALF and HOL. Technical Report 461, University of Cambridge, Computer Laboratory.

31

Jeffrey J. Joyce , Carl-Johan H. Seger, Linking BDD-based symbolic evaluation to interactive theorem-proving, Proceedings of the 30th international conference on Design automation, p.469-474, June 14-18, 1993, Dallas, Texas, United States [doi>10.1145/157485.164981]

32

32. Kort S, Tahar S, Curzon P (2003) Hierarchical formal verification using a hybrid tool. Softw Tools Technol Trans 4(3):313-322.

33

33. Lind-Nielsen J, BuDDY--A binary decision diagram package, http://www.itu.dk/research/buddy/

34

34. Melham T (2004) Integrating model checking and theorem proving in a reflective functional language. In: Kirchner H, Ringeissen C (eds) Integrated formal methods, vol. 2999 of Lecture Notes in Computer Science, Springer-Verlag, pp. 36-39.

35

T. Melham, Higher order logic and hardware verification, Cambridge University Press, New York, NY, 1993

36

36. Mhamdi T, Tahar S (2004) Providing automated verification in HOL using MDGs. In: Wang F (ed) Automated technology for verification and analysis, vol. 3299 of Lecture Notes in Computer Science, Springer-Verlag, pp. 278-293.

37

Laurence C. Paulson, ML for the working programmer, Cambridge University Press, New York, NY, 1991

38

S. Rajan , Natarajan Shankar , Mandayam K. Srivas, An Integration of Model Checking with Automated Proof Checking, Proceedings of the 7th International Conference on Computer Aided Verification, p.84-97, July 03-05, 1995

39

Natarajan Shankar, Combining Theorem Proving and Model Checking through Symbolic Analysis, Proceedings of the 11th International Conference on Concurrency Theory, p.1-16, August 22-25, 2000

40

Natarajan Shankar, Using Decision Procedures with a Higher-Order Logic, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.5-26, September 03-06, 2001

41

Sofiène Tahar , Paul Curzon , Jianping Lu, Three Approaches to Hardware Verification: HOL, MDG and VIS Compared, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.433-450, November 04-06, 1998

42

42. Tammet T (October 1997) Gandalf version c-1.0c reference manual, http://www.cs.chalmers. sr/~tammet/

43

Laurent Théry, A Machine-Checked Implementation of Buchberger's Algorithm, Journal of Automated Reasoning, v.26 n.2, p.107-137, February 2001 [doi>10.1023/A:1026518331905]

44

Tomás E. Uribe, Combinations of Model Checking and Theorem Proving, Proceedings of the Third International Workshop on Frontiers of Combining Systems, p.151-170, March 22-24, 2000

45

45. Xiong H (January 2002) Providing a formal linkage between MDG and HOL based on a verified MDG system. Ph.D. thesis, School of Computing Science, Middlesex University, UK.

46

Haiyan Xiong , Paul Curzon , Sofiène Tahar, Importing MDG Verification Results into HOL, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.293-310, September 01, 1999

47

Editors:, TPHOLs 2000: Supplemental Proceedings, Oregon Graduate Institute School of Science & Engineering, 2000

48

48. Xiong H, Curzon P, Tahar S, Blandford A (September 2001) Proving existential theorems when importing results from MDG to HOL. In: Boulton R, Jackson P (eds) TPHOLs 2001 Supplemental Proceedings, Informatic Research Report EDI-INF-RR-0046, pp. 384-399.

49

49. Zhou Z, Boulerice N (1996) MDG Tools (V1.0) User Manual. University of Montreal, Dept. D'IRO.

50

Z. Zhou , Xiaoyu Song , Sofiène Tahar , Eduard Cerny , Francisco Corella , Michel Langevin, Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, p.233-247, November 06-08, 1996

Repository Staff Only: item control page