%0 Book Section %1 loepucl5137 %A Xiong, H. %A Curzon, P. %A Tahar, S. %A Blandford, A. %B Integrated Formal Methods %C Heidelberg %D 2002 %E Goos, G. %E Hartmanis, J. %E van Leeuwen, J. %I Springer Berlin %K deductive-theorem-proving hardware-verification hybrid-verification-systems symbolic-state-enumeration usability-verification %N 2335 %P 205--224 %T Formally linking MDG and HOL based on a verified MDG system %U http://eprints.ucl.ac.uk/5137/ %X We describe an approach for formally linking a symbolic state enumeration system and a theorem proving system based on a verified version of the former. It has been realized using a simplified version of the MDG system and the HOL system. Firstly, we have verified aspects of correctness of a simplified version of the MDG system. We have made certain that the semantics of a program is preserved in those of its translated form. Secondly, we have provided a formal linkage between the MDG system and the HOL system based on importing theorems. The MDG verification results can be formally imported into HOL to form a HOL theorem. Thirdly, we have combined the translator correctness theorems and importing theorems. This allows the MDG verification results to be imported in terms of a high level language (MDG-HDL) rather than a low level language. We also summarize a general method to prove existential theorems for the design. The feasibility of this approach is demonstrated in a case study that integrates two applications: hardware verification (in MDG) and usability verification (in HOL). A single HOL theorem is proved that integrates the two results.

@incollection{loepucl5137, abstract = {We describe an approach for formally linking a symbolic state enumeration system and a theorem proving system based on a verified version of the former. It has been realized using a simplified version of the MDG system and the HOL system. Firstly, we have verified aspects of correctness of a simplified version of the MDG system. We have made certain that the semantics of a program is preserved in those of its translated form. Secondly, we have provided a formal linkage between the MDG system and the HOL system based on importing theorems. The MDG verification results can be formally imported into HOL to form a HOL theorem. Thirdly, we have combined the translator correctness theorems and importing theorems. This allows the MDG verification results to be imported in terms of a high level language (MDG-HDL) rather than a low level language. We also summarize a general method to prove existential theorems for the design. The feasibility of this approach is demonstrated in a case study that integrates two applications: hardware verification (in MDG) and usability verification (in HOL). A single HOL theorem is proved that integrates the two results.}, added-at = {2008-10-24T14:29:07.000+0200}, address = {Heidelberg}, author = {Xiong, H. and Curzon, P. and Tahar, S. and Blandford, A.}, biburl = {https://www.bibsonomy.org/bibtex/2ec11cf40d7478fe9f37970344d625b69/uclic}, booktitle = {Integrated Formal Methods}, description = {UCLIC eprints as of October 2008}, editor = {Goos, G. and Hartmanis, J. and van Leeuwen, J.}, interhash = {6a1984472d9479cb4294e6abb18e6b8b}, intrahash = {ec11cf40d7478fe9f37970344d625b69}, keywords = {deductive-theorem-proving hardware-verification hybrid-verification-systems symbolic-state-enumeration usability-verification}, note = {The original publication is available at www.springerlink.com}, number = 2335, pages = {205--224}, publisher = {Springer Berlin}, series = {Lecture Notes in Computer Science}, timestamp = {2008-10-24T14:39:26.000+0200}, title = {Formally linking MDG and HOL based on a verified MDG system}, url = {http://eprints.ucl.ac.uk/5137/}, year = 2002 }