An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model

Citation:
Ferreira M, Oliveira JN.  2009.  An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model. SBMF - 12th Brazilian Symposium on Formal Methods. 5902:153-169.

Tertiary Title:

LNCS

Date Presented:

August

Abstract:

Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel R©Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together.

Citation Key:

FO09a

DOI:

10.1007/978-3-642-10452-7_11

PreviewAttachmentSize
paper_37.pdf220.87 KB