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. 83116. ISSN 09259856

Text (application/pdf)
304kBFMSD2007.pdf  Accepted Version 
Official URL: http://dx.doi.org/10.1007/s107030060017y
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 lowlevel 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/s107030060017y 
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 , CarlJohan H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings of the 37th conference on Design automation, p.201206, June 0509, 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.2742, September 0306, 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, SpringerVerlag, pp. 171187.
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.4766, August 2023, 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. 187196.
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.129156, June 2224, 1992
7
Randal E. Bryant, GraphBased Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677691, August 1986 [doi>10.1109/TC.1986.1676819]
8
Randal E. Bryant, Symbolic Boolean manipulation with ordered binarydecision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293318, Sept. 1992 [doi>10.1145/136035.136043]
9
9. Buchberger B (2004) Towards the automated synthesis of a Gröbner bases algorithm. RACSAM 98(12):6575.
10
10. Butterworth R, Blandford AE, Duke D (2000) Demonstrating the cognitive plausibility of interactive systems. Formal Asp Comput 12:237259.
11
11. Byrne M, Bovair S (1997) A working memory model of a common procedural error. Cogn Sci 21(1):3161.
12
12. Camilleri A, Gordon M, Melham T (September 1986) Hardware verification using Higherorder 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. 4367.
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.185214, April 1986 [doi>10.1145/5397.30847]
14
ChingTsun Chou , Doron Peled, Formal Verification of a PartialOrder Reduction Technique for Model Checking, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.241257, March 2729, 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.746, 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 postcompletion errors. In: Palanque P, Paternó F (eds) Participants Proceedings of DSVIS 2000: 7th International Workshop on Design, Specification and Verification of Interactive Systems, at the 22nd International Conference on Software Engineering, Limerick, Ireland, Kluwer, pp. 293308.
19
Paul Curzon , Ann Blandford, Detecting Multiple Classes of User Errors, Proceedings of the 8th IFIP International Conference on Engineering for HumanComputer Interaction, p.5772, May 1113, 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ïtMohamed O (1998) Verification of the MDG components library in HOL. In: Grundy J, Newey M (eds) Theorem proving in higherorder logics: Emerging trends, Department of Computer Science, The Australian National University, pp. 3146.
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.7892, March 25April 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, SpringerVerlag.
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.179196, August 1418, 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.279294, December 1998 [doi>10.1023/A:1006023127567]
28
Scott Hazelhurst , CarlJohan H. Seger, Symbolic Trajectory Evaluation, Formal Hardware Verification  Methods and Systems in Comparison, p.378, January 1997
29
André Heck, Introduction to Maple, SpringerVerlag 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 , CarlJohan H. Seger, Linking BDDbased symbolic evaluation to interactive theoremproving, Proceedings of the 30th international conference on Design automation, p.469474, June 1418, 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):313322.
33
33. LindNielsen J, BuDDYA 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, SpringerVerlag, pp. 3639.
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, SpringerVerlag, pp. 278293.
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.8497, July 0305, 1995
39
Natarajan Shankar, Combining Theorem Proving and Model Checking through Symbolic Analysis, Proceedings of the 11th International Conference on Concurrency Theory, p.116, August 2225, 2000
40
Natarajan Shankar, Using Decision Procedures with a HigherOrder Logic, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.526, September 0306, 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 ComputerAided Design, p.433450, November 0406, 1998
42
42. Tammet T (October 1997) Gandalf version c1.0c reference manual, http://www.cs.chalmers. sr/~tammet/
43
Laurent Théry, A MachineChecked Implementation of Buchberger's Algorithm, Journal of Automated Reasoning, v.26 n.2, p.107137, 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.151170, March 2224, 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.293310, 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 EDIINFRR0046, pp. 384399.
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 ComputerAided Design, p.233247, November 0608, 1996
Repository Staff Only: item control page