Title :
Linking VDM and Z
Author :
Woodcock, Jim ; Freitas, Leo
Author_Institution :
Univ. of York, York
fDate :
March 31 2008-April 3 2008
Abstract :
The International Grand Challenge in Verified Software is benchmarking current verification technology by conducting a series of experiments, and one such experiment is to build a verified POSIX-compliant flash filestore. An objective of this experiment is to combine different formal methods, and this raises issues about the different logics used. One significant area of difference is in the treatment of undefined expressions, and we show how this difference can be overcome using a unifying theory. This then allows us to use a theorem proverfor Z to verify theorems about a data type specified and refined in VDM.
Keywords :
flash memories; formal verification; storage management; International Grand Challenge in Verified Software; POSIX-compliant flash filestore; formal methods; theorem prover; unifying theory; verification technology; Computer science; Costs; Hardware; Joining processes; Large-scale systems; Logic; Programming; Software maintenance; Software performance; Software tools; Grand Challenge; POSIX; VDM; Z; file store; linking theories; software verification;
Conference_Titel :
Engineering of Complex Computer Systems, 2008. ICECCS 2008. 13th IEEE International Conference on
Conference_Location :
Belfast
Print_ISBN :
0-7695-3139-3
DOI :
10.1109/ICECCS.2008.36
