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 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. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Ferreira, M. A., & Oliveira, J. N. (2009). An integrated formal methods tool-chain and its application to verifying a file system model. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5902 LNCS, pp. 153–169). https://doi.org/10.1007/978-3-642-10452-7_11
Mendeley helps you to discover research relevant for your work.