UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Formally linking MDG and HOL based on a verified MDG system

Xiong, H; Curzon, P; Tahar, S; Blandford, A; (2002) Formally linking MDG and HOL based on a verified MDG system. In: Goos, G and Hartmanis, J and van Leeuwen, J, (eds.) Integrated Formal Methods. (pp. 205-224). Springer Berlin: Heidelberg.

Full text not available from this repository.


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.

Type: Book chapter
Title: Formally linking MDG and HOL based on a verified MDG system
ISBN-13: 978-3-540-43703-1
DOI: 10.1007/3-540-47884-1_12
Additional information: Imported via OAI, 7:29:01 6th Mar 2008
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/98444
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item