An integrated formal methods tool-chain and its application to verifying a file...

• Author(s): Ferreira, Miguel A. ; Oliveira, José Nuno Fonseca
• Date: 2009
• Persistent ID: http://hdl.handle.net/1822/17801
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Grand challenges in computing; Formal methods
• Document Type: Article
• Language: English

Description

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.